Huge commit:

[helm.git] / components / tactics / auto.ml

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 92d66ef726ab7d245f0072c9aec81f3f7e85ed1d..5f110bc4c39030d22f6f051525c097ba00391fa0 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -84,7 +84,7 @@ let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
 
 let is_unit_equation context metasenv oldnewmeta term = 
   let head, metasenv, args, newmeta =
-    ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+    TermUtil.saturate_term oldnewmeta metasenv context term 0
   in
   let propositional_args = 
     HExtlib.filter_map
@@ -246,7 +246,7 @@ let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
 
 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = 
   let head, metasenv, args, newmeta =
-    ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+    TermUtil.saturate_term oldnewmeta metasenv context term 0
   in
   let propositional_args = 
     HExtlib.filter_map
@@ -430,7 +430,7 @@ let new_metasenv_and_unify_and_t
  context term' ty termty goal_arity 
 =
  let (consthead,newmetasenv,arguments,_) =
-   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+   TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
  let term'' = 
    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
  in
@@ -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);;