X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=ae9143dabf849ed29f1d9c5c9e41b2f8114c9230;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=23a8b8e6755c34071a78bdd1419a9ea5e6118808;hpb=2e5bbbe9aaae0b0d2b2ad7b91b17dbc25ec21929;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 23a8b8e67..ae9143dab 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -92,11 +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 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option
@@ -139,11 +145,20 @@ type ('term, 'ident) tactical =
       (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
   | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
 
-type ('term, 'ident) statement =
+
+type ('term, 'ident) code =
   | Command of loc * 'term command
   | Macro of loc * 'term macro 
       (* Macro are substantially queries, but since we are not the kind of
        * peolpe that like to push "start" to turn off the computer 
        * we added this command *)
   | Tactical of loc * ('term, 'ident) tactical
+             
+type ('term, 'ident) comment =
+  | Note of loc * string
+  | Code of loc * ('term, 'ident) code
+             
+type ('term, 'ident) statement =
+  | Executable of loc * ('term, 'ident) code
+  | Comment of loc * ('term, 'ident) comment