X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite%2FgrafiteAst.ml;h=9c5d56024917795facba7653bc89d1019a192754;hb=e6454d89343d6ad3195360a0d5a584d5ad3a3575;hp=7108a323a07c0b38e418eb9890c7bd074276682c;hpb=666e2a3fcbfffd2df99650e3404965e95e6b352b;p=helm.git

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 7108a323a..9c5d56024 100644
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -98,7 +98,9 @@ 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 option * 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 ]
 
@@ -114,7 +116,7 @@ type 'term macro =
   (* real macros *)
   | Check of loc * 'term 
   | Hint of loc
-  | Inline of loc * string (* the string is a URI or a base-uri *)
+  | Inline of loc * string * string (* URI or base-uri, name prefix *) 
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)