From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 20 May 2006 10:42:04 +0000 (+0000)
Subject: fixed wrong calculation of free_metas
X-Git-Tag: make_still_working~7346
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c04c7b4635b43c03f305bb1feadcb89496355111;p=helm.git

fixed wrong calculation of free_metas
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index c8e74642b..3bc8eb25b 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1766,11 +1766,6 @@ let saturate
           (ProofEngineHelpers.compare_metasenvs 
             ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
-      let free_metas = 
-        List.filter (fun i -> i <> goalno)
-          (ProofEngineHelpers.compare_metasenvs 
-            ~oldmetasenv:metasenv ~newmetasenv:proof_menv)
-      in
       let goal_proof, side_effects_t = 
         let initial = Equality.build_proof_term newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
@@ -1801,6 +1796,11 @@ let saturate
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
          * what mi pare buono, sostituisce solo le meta farlocche *)
       let side_effects_t = List.map replace side_effects_t in
+      let free_metas = 
+        List.filter (fun i -> i <> goalno)
+          (ProofEngineHelpers.compare_metasenvs 
+            ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
+      in
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1826,11 +1826,17 @@ let saturate
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
       let _ = 
-        let ty,_ =
+        try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
             CicUniv.empty_ugraph
-        in
-        ty
+        with 
+        | CicUtil.Meta_not_found _ 
+        | CicTypeChecker.TypeCheckerFailure _ 
+        | CicTypeChecker.AssertFailure _ 
+        | Invalid_argument "list_fold_left2" as exn ->
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+            prerr_endline (CicPp.pp goal_proof names);
+            raise exn
       in
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof