From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- tactics/eqdecide.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/eqdecide.ml') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index df60f2c66..bac3980d2 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -176,7 +176,7 @@ let solveEqBranch rectype = Proofview.tclORELSE begin Proofview.Goal.enter { enter = begin fun gl -> - let concl = pf_nf_concl gl in + let concl = pf_concl gl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -202,7 +202,7 @@ let decideGralEquality = Proofview.tclORELSE begin Proofview.Goal.enter { enter = begin fun gl -> - let concl = pf_nf_concl gl in + let concl = pf_concl gl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app sigma (pf_compute gl typ) in -- cgit v1.2.3