elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 1ec71be92481e826763b18e81f4c6cb7bd244ad6..b5e75712fb7ea6a6e7c467eb0f3b3f0029efe3b3 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -55,7 +55,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Decompose of loc * 'ident list
   | Demodulate of loc
   | Destruct of loc * 'term
-  | Elim of loc * 'term * 'term option * int option * 'ident list
+  | Elim of loc * ('term, 'lazy_term, 'ident) pattern * 'term option * 
+            int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
   | Exists of loc