New declarative tactic "we proceed by cases on t to prove t'".

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

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 7a9b7b5ae05f7099244d3a7c70fa189fc5b85040..d6dfa53a65dc88e1a4b744e9ef0147539ee01f05 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -93,6 +93,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