1) variables occurring only in proofs anre not relocated

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 445eccdbc2f217565c67b5f319cb2652c105066e..e12b1f8a7a1b23591749e6de244da6804152e15b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1692,7 +1692,7 @@ let saturate
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let goal = [], metasenv, type_of_goal in
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, type_of_goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -1760,6 +1760,7 @@ let saturate
     (goalproof,newproof,subsumption_subst, proof_menv) ->
       prerr_endline "OK, found a proof!";
       prerr_endline (Equality.pp_proof names goalproof newproof);
+      prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
       let side_effects = 
@@ -1771,7 +1772,7 @@ let saturate
         let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
-prerr_endline (CicPp.pp goal_proof names);
+(*prerr_endline (CicPp.pp goal_proof names);*)
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
@@ -1790,6 +1791,8 @@ prerr_endline (CicPp.pp goal_proof names);
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) proof_menv 
       in
+prerr_endline ("RIMPIAZZATO CON " ^ match free_meta with None -> "?" | Some m -> CicPp.ppterm m);
+
       let replace where = 
         ProofEngineReduction.replace_lifting 
           ~equality:(=) ~what ~with_what ~where
@@ -1803,6 +1806,7 @@ prerr_endline (CicPp.pp goal_proof names);
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
+prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) );
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1827,6 +1831,7 @@ prerr_endline (CicPp.pp goal_proof names);
       let final_subst = 
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
+prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
       let _ = 
         try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
@@ -1837,7 +1842,7 @@ prerr_endline (CicPp.pp goal_proof names);
         | CicTypeChecker.AssertFailure _ 
         | Invalid_argument "list_fold_left2" as exn ->
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-            prerr_endline (CicPp.pp goal_proof names);
+(*            prerr_endline (CicPp.pp goal_proof names); *)
             raise exn
       in
       let proof, real_metasenv =