diff options
| author | Hugo Herbelin | 2014-10-20 23:34:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-20 23:46:40 +0200 |
| commit | da462f8a2b59a3d5ddd9f09add8a75f8e2624c9a (patch) | |
| tree | 195e24524bee1e699238d12881f4a0082d307cb8 | |
| parent | 98f3abb83a26b85092140e8850fd372622f24bdb (diff) | |
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.
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files 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 |