...

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

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 625beb839834c27a21b0b5bc17aec3a01afa3629..1d5d9783fb3bdf4a7df250f67f5b3691e6990183 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1249,31 +1249,33 @@ let build_proof
           eq_uri goalproof initial type_of_goal side_effects
           context proof_menv
       in
-(*       prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+      (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof 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
       in
       (* replacing fake mets with real ones *)
-(*       prerr_endline "replacing metas..."; *)
+      (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
       let goal_proof_menv, what, with_what,free_meta = 
         List.fold_left 
           (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
              match uniq with
                | Some m -> 
-(*                    acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *)
-                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq
+(*                     acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq  *)
+                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2,
+                     (Cic.Meta(i,irl))::acc3, uniq
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) 
           (List.filter 
-           (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
+           (fun (i,_,_) -> 
+             List.mem i metas_still_open_in_proof
+             (*&& not(List.mem i metas_still_open_in_goal)*)) 
            proof_menv)
       in
       let replace where = 
@@ -1293,8 +1295,9 @@ let build_proof
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
-(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int
- * free_metas) ); *)
+      (* prerr_endline 
+       *   ("freemetas: " ^ 
+       *   String.concat "," (List.map string_of_int free_metas) ); *)
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1340,13 +1343,20 @@ let build_proof
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
             raise exn
       in
+
+      let metas_of_proof = Utils.metas_of_term goal_proof in
+
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
       let open_goals = 
+        HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) 
+      in
+(*
         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
+*)
 (*
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"