X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAst.ml;h=e75e53867aa88306d06dedfe5ee1fff9f2b9efe8;hb=3f586b01da59fe16b3d7f37da28bdd71f2225131;hp=d6dfa53a65dc88e1a4b744e9ef0147539ee01f05;hpb=172588c02ff4d9ed5cc03265c2bd6a36f8a0f5da;p=helm.git

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index d6dfa53a6..e75e53867 100644
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -77,9 +77,10 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | LetIn of loc * 'term * 'ident
   | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern 
   | Reflexivity of loc
+  | Rename of loc * 'ident list * 'ident list
   | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Rewrite of loc * direction * 'term *
-      ('term, 'lazy_term, 'ident) pattern
+      ('term, 'lazy_term, 'ident) pattern * 'ident list
   | Right of loc
   | Ring of loc
   | Split of loc