From: Enrico Tassi 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! "; 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