From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- tactics/eqdecide.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'tactics/eqdecide.ml') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index a96656d3a..16e0d9684 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -178,7 +178,6 @@ let solveEqBranch rectype = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - let concl = EConstr.of_constr concl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -205,7 +204,6 @@ let decideGralEquality = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - let concl = EConstr.of_constr concl 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