Declare ML Module "autocontra".

Grammar tactic simple_tactic :=
	[ "Auto_Contra" identarg($id)] ->
	[(TRY (auto_contra $id))].

Grammar tactic simple_tactic :=
	[ "Auto_Contra"] ->
	[(TRY (auto_contran))].