(* Tactic syntax *)

Grammar tactic simple_tactic :=
	[ "NComp2" command:command($i) command:command($j)] ->
	[let $1 = <<(nat_compare2 $i $j)>> in
	 <:tactic:< Cut $1 ;
		[Destruct 1; [Intro | Destruct 1; Intro] | Auto]>>].

Grammar tactic simple_tactic :=
	[ "NComp" command:command($i) command:command($j)] ->
	[let $1 = <<(nat_compare $i $j)>> in
	 <:tactic:< Cut $1 ;
		 [Destruct 1; Intro |
		  Auto]>>].

Grammar tactic simple_tactic :=
	[ "Induction_clear" identarg($i)] ->
	[ <:tactic:<Induction $i; Clear $i>>].

Grammar tactic simple_tactic :=
	[ "Injection_clear" identarg($i)] ->
	[ <:tactic:<Injection $i; Clear $i; Intros>>].