X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=ae9143dabf849ed29f1d9c5c9e41b2f8114c9230;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=692d4679e85b012e6da2018d38815c7983b9fae0;hpb=157f12c3cb9cc4ed5ba9d1e46c64a593c7fd9481;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 692d4679e..ae9143dab 100644
--- 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