X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=51b86fa5e092db484f01737a5113db82087f8adc;hb=bde29698c58eb36166753a30765a92e602e9cc78;hp=db08a6038f86bcf08c23f6fc33ec3994ef79010e;hpb=c2d8fcd86793151c8cf24f45fc3064b97f16f596;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index db08a6038..51b86fa5e 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -87,9 +87,9 @@ let tactic_of_ast status ast =
       Tactics.demodulate 
 	~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
-  | GrafiteAst.Elim (_, what, using, depth, names) ->
+  | GrafiteAst.Elim (_, what, using, pattern, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
-        what
+        ~pattern what
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what