From da462f8a2b59a3d5ddd9f09add8a75f8e2624c9a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Oct 2014 23:34:45 +0200
Subject: Removing re-typecheking from "refine" in no-check mode of the new
 convert_concl/convert_hyp. This was actually probably the main source of
 inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than nf_enter, as
 suspected in 3c2723f.

---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f66c18822f..274ec4cd49 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -133,7 +133,7 @@ let convert_concl ?(check=true) ty k =
       end else sigma in
     Tacticals.New.tclTHEN
       (Proofview.V82.tclEVARS sigma)
-      (Proofview.Refine.refine (fun sigma ->
+      (Proofview.Refine.refine ~unsafe:true (fun sigma ->
         let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ty in
         (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
   end
@@ -145,7 +145,7 @@ let convert_hyp ?(check=true) d =
     let ty = Proofview.Goal.raw_concl gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Proofview.Refine.refine (fun sigma -> Evarutil.new_evar env sigma ~principal:true ty)
+    Proofview.Refine.refine ~unsafe:true (fun sigma -> Evarutil.new_evar env sigma ~principal:true ty)
   end
 
 let convert_concl_no_check = convert_concl ~check:false
-- 
cgit v1.2.3