Demodulate_tac now depends on the universe

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)

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 92d66ef726ab7d245f0072c9aec81f3f7e85ed1d..3c35013aa37a6b0923cc9868e8db2ff785cdc5d6 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -1190,14 +1190,14 @@ let eq_of_goal = function
 ;;
 
 (* DEMODULATE *)
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
+let demodulate_tac ~dbd ~universe (proof,goal)= 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let initgoal = [], [], ty in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
-     init_cache_and_tables dbd true true Universe.empty (proof,goal) in
+     init_cache_and_tables dbd false true universe (proof,goal) in
   let equalities = (Saturation.list_of_passive passive) in
   (* we demodulate using both actives passives *)
   let table = 
@@ -1232,7 +1232,8 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
+let demodulate_tac ~dbd ~universe = 
+  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
 
 
 

diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index d749a26af175a8221d2d655794594ad0536873fd..d8efa613e1ae599242177294fd5b4b9b209d4065 100644 (file)
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -37,4 +37,7 @@ val applyS_tac:
   universe:Universe.universe ->
   ProofEngineTypes.tactic
 
-val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate_tac : 
+  dbd:HMysql.dbd -> 
+  universe:Universe.universe ->
+  ProofEngineTypes.tactic

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 3379fbe77b14503420f1954e65515250695ff773..88179e4c8724f3bb1b9e9e61868ebeed29606f21 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -26,7 +26,8 @@ val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->
   ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate : dbd:HMysql.dbd -> 
+  universe:Universe.universe -> ProofEngineTypes.tactic
 val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->