Demodulate_tac now depends on the universe

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index a8ee6752ce9cc5a54e45f0add54acee68504422d..df01f8467f2778dbf3a33db297830116dcd0c02b 100644 (file)
--- 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)