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 c8e74642b6cbdae7be949c101c239ee27cd3d5b8..3bc8eb25bf2cfb13fce3641b6b40cf793d80ecc1 100644 (file)
--- 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