From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 7 Sep 2007 10:04:01 +0000 (+0000)
Subject: disabled coercions when refining paramod proofs (attemt to understand the slowdown... 
X-Git-Tag: 0.4.95@7852~217
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=370c85cb0257dc6fe1cf30c5f4597ba43eb5d3e6;p=helm.git

disabled coercions when refining paramod proofs (attemt to understand the slowdown of night-tests)
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 6e7922019..9739f1ccf 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1361,20 +1361,33 @@ let build_proof
     prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
     raise exn
   in
+  let old_insert_coercions = !CicRefine.insert_coercions in
   let goal_proof,goal_ty,real_menv,_ = 
     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
     try
             debug_print (lazy (CicPp.ppterm goal_proof));
-      CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+            CicRefine.insert_coercions := false;
+            let res = 
+              CicRefine.type_of_aux' 
+                real_menv context goal_proof CicUniv.empty_ugraph
+            in
+            CicRefine.insert_coercions := old_insert_coercions;
+            res
     with 
       | CicRefine.RefineFailure s 
       | CicRefine.Uncertain s 
       | CicRefine.AssertFailure s as exn -> 
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names (Lazy.force s) exn
       | CicUtil.Meta_not_found i as exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
       | Invalid_argument "list_fold_left2" as exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names "Invalid_argument: list_fold_left2" exn 
+      | exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
+          raise exn
   in     
   let subst_side_effects,real_menv,_ = 
     try