- implemented CicPushParser which parser CIC objects using Expat

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index d4e94b28bea16ce511ca4341b6489378becedde4..e01b7e7edf2985559668d517fedd7be60781b08b 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -38,7 +38,7 @@ type loc = CicAst.location
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | Auto of loc
+  | Auto of loc * int option
   | Assumption of loc
   | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
   | Change_pattern of loc * 'term pattern * 'term * 'ident option
@@ -97,6 +97,7 @@ type 'term macro =
   | Check of loc * 'term 
   | Hint of loc
   | Match of loc * 'term 
+  | Instance of loc * 'term 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option