]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAst.ml
fixed Whelp stuff
[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml
index a7b0fbeafa523dc402ab4df99cc9e93c8aefd215..ae9143dabf849ed29f1d9c5c9e41b2f8114c9230 100644 (file)
@@ -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
@@ -92,6 +92,13 @@ 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 
@@ -138,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