;;
(* 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 =
~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);;