fixed Whelp stuff

[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 692d4679e85b012e6da2018d38815c7983b9fae0..ae9143dabf849ed29f1d9c5c9e41b2f8114c9230 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -92,12 +92,17 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 type print_kind = [ `Env | `Coer ]
 
 type 'term macro = 
+  (* Whelp's stuff *)
+  | WHint of loc * 'term 
+  | WMatch of loc * 'term 
+  | WInstance of loc * 'term 
+  | WLocate of loc * string
+  | WElim of loc * 'term
+  (* real macros *)
   | Abort of loc
   | Print of loc * string
   | 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