X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteEngine.ml;h=df01f8467f2778dbf3a33db297830116dcd0c02b;hb=b0612e00b2a905510439d9a6e8908497c1b74c61;hp=a8ee6752ce9cc5a54e45f0add54acee68504422d;hpb=18c16056c2858405c899ab027ec7e7ba2cc967b4;p=helm.git

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index a8ee6752c..df01f8467 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -86,7 +86,9 @@ let tactic_of_ast status ast =
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
-  | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
+  | GrafiteAst.Demodulate _ -> 
+      Tactics.demodulate 
+	~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)