X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=e75e53867aa88306d06dedfe5ee1fff9f2b9efe8;hb=0582a602f0b1d6f5430326893a473d78b0aa7dfd;hp=7a9b7b5ae05f7099244d3a7c70fa189fc5b85040;hpb=9fce3bebddf47429f6fcab726f11dafbf3295749;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 7a9b7b5ae..e75e53867 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/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
@@ -93,6 +94,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | We_need_to_prove of loc * 'term * 'ident option * 'term option
   | Bydone of loc * 'term option 
   | We_proceed_by_induction_on of loc * 'term * 'term
+  | We_proceed_by_cases_on of loc * 'term * 'term
   | Byinduction of loc * 'term * 'ident
   | Thesisbecomes of loc * 'term
   | Case of loc * string * (string * 'term) list