From 1cb6d3b235b03ccba046dee70b22d9f2e8dd8192 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 15 Jul 2009 10:03:21 +0000 Subject: - Fixing bug #2139 (kernel-based test of well-formation of elimination predicate called from proof refiner was failing because it was not aware of evars instantiation; I added a nf_evar in 8.2 branch but for the trunk, I propose to remove the elimination predicate well-formation test; we therefore assume that tactics build correct elimination predicates in Case, is it not too much demanding?). - Seized the opportunity to remove dead kernel code about non dependent elimination predicates (all predicates are stored dependent by default since a few years now). - Anecdotic complement to commit 12229 (removal of obsolete comment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/logic.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index b8ba88185..f1f33930e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -436,12 +436,11 @@ and mk_casegoals sigma goal goalacc p c = let env = evar_env goal in let (acc',ct) = mk_hdgoals sigma goal goalacc c in let (acc'',pt) = mk_hdgoals sigma goal acc' p in - let pj = {uj_val=p; uj_type=pt} in let indspec = try find_mrectype env sigma ct with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = - type_case_branches_with_names env indspec pj c in + type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty) -- cgit v1.2.3