- 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

0 files changed, 0 insertions, 0 deletions