call paramod instead of solve_Rewrite

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 45cab35026a4dd196ee765c4cd742cf3918da073..61ae8bd791fbbe173f62fe1f5f60c7150521e302 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = false;;
+let debug = true;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
@@ -404,7 +404,7 @@ let init_cache_and_tables
              c metasenv [] context st (Some head), maxmeta)
        (automation_cache,CicMkImplicit.new_meta metasenv subst) ct
     in
-(*     AutomationCache.pp_cache automation_cache; *)
+    AutomationCache.pp_cache automation_cache;
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache
@@ -440,7 +440,7 @@ let init_cache_and_tables
          AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
        automation_cache s_t_ty
     in
-(*     AutomationCache.pp_cache automation_cache; *)
+    AutomationCache.pp_cache automation_cache;
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache_add_list cache_empty context t_ty
@@ -1091,9 +1091,37 @@ let apply_smart_aux
        (PrimitiveTactics.apply_tac term'')
        (proof''',goal) 
    in
+
+
+   let (_,m,_,_,_,_ as p) = 
+        let pu,metasenv,subst,proof,px,py = proof'''' in
+        let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+        let proof'''' = pu,metasenv,subst,proof,px,py in
+        let univ, params = params in
+        let use_context = bool params "use_context" true in 
+        let universe, (active,passive,bag), cache =
+         init_cache_and_tables ~use_library:false ~use_context
+           automation_cache univ (proof'''',newmeta)
+        in
+        match
+          Saturation.given_clause bag (proof'''',newmeta) active passive 
+            20 2 infinity
+        with 
+          | None, active, passive, bag -> 
+              raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
+          | Some(subst',(pu,metasenv,_,proof,px, py),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              pu,metasenv,subst,proof,px,py
+   in
+
+(*
    let (_,m,_,_,_,_ as p),_ = 
       solve_rewrite ~params ~automation_cache (proof'''',newmeta)
    in
+*)
+
    let open_goals = 
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m
    in