From 2f4cf6f683207d7e755f8ba067f86c2f98f778fb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 Sep 2007 10:04:01 +0000 Subject: [PATCH] disabled coercions when refining paramod proofs (attemt to understand the slowdown of night-tests) --- .../tactics/paramodulation/saturation.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 6e7922019..9739f1ccf 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/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 -- 2.39.2