some hacks to make the sequent window pretty nice

[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 e01b7e7edf2985559668d517fedd7be60781b08b..692d4679e85b012e6da2018d38815c7983b9fae0 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -140,11 +140,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