content2Procedural.ml: "Intros+LetTac" ok

[helm.git] / components / grafite / grafiteAst.ml

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index a4d357702925e86a5fb8b4b5e8d643e3b77f54fa..8979129158b34bcd8a9ffa03577dca64bfb399e9 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -98,13 +98,17 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
   | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
   | RewritingStep of
-     loc * 'term option * 'term  *
-      [ `Term of 'term | `Auto of (string * string) list ] * Cic.name option
+     loc * (string option * 'term) option * 'term  *
+      [ `Term of 'term | `Auto of (string * string) list ] *
+      bool (* last step*)
   
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
 type print_kind = [ `Env | `Coer ]
 
+type style = Declarative
+           | Procedural
+
 type 'term macro = 
   (* Whelp's stuff *)
   | WHint of loc * 'term 
@@ -115,7 +119,7 @@ type 'term macro =
   (* real macros *)
   | Check of loc * 'term 
   | Hint of loc
-  | Inline of loc * string * string (* URI or base-uri, name prefix *) 
+  | Inline of loc * style * string * string (* URI or base-uri, name prefix *) 
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)