X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=8813e498bed94ae6425757af2e4d88ed1c025794;hb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;hp=3746403d951ea382e8360c2fcd2f933dc0f1cc07;hpb=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 3746403d9..8813e498b 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -89,9 +89,9 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.AutoBatch (_,params) ->
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
 	~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Cases (_, what, (howmany, names)) ->
+  | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
       Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
-        what
+        ~pattern what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id