procedural : some improvements.

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index ab98132210238daf670872dacbb356cf6817c9df..1714bf470ac8c070e97a98e3327eee7a4183bb50 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -80,15 +80,9 @@ 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