X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=b5e75712fb7ea6a6e7c467eb0f3b3f0029efe3b3;hb=8ae990161006978a019f0afda4ff8d56a78d1fd0;hp=1ec71be92481e826763b18e81f4c6cb7bd244ad6;hpb=f275a4daa42f8ab455020ec5a7ce7bf69b460c37;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 1ec71be92..b5e75712f 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/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