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=ab98132210238daf670872dacbb356cf6817c9df;hpb=77d56df4d446307199a9d4e03478260c6c63baf8;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ab9813221..51b86fa5e 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -80,22 +80,16 @@ let tactic_of_ast status ast =
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
-  | GrafiteAst.Decompose (_, types, what, names) -> 
-      let to_type = function
-         | GrafiteAst.Type (uri, typeno) -> uri, Some typeno
-	 | GrafiteAst.Ident _            -> assert false
-      in
-      let user_types = List.rev_map to_type types in
-      let dbd = LibraryDb.instance () in
+  | GrafiteAst.Decompose (_, names) ->
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+      Tactics.decompose ~mk_fresh_name_callback ()
   | GrafiteAst.Demodulate _ -> 
       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
@@ -179,7 +173,8 @@ let tactic_of_ast status ast =
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
-     Declarative.existselim t id1 t1 id2 t2
+     Declarative.existselim ~dbd:(LibraryDb.instance())
+      ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->