Complement to 12347 and 12348 on the extended syntax of case/elim.

Don't change the semantics of "case 1" and forbid the use of numbers
to refer to non-dependent quantified hypotheses in the more general
forms that are synonymous of "destruct" (don't want to commit to a
syntax for non-dependent quantified hypotheses which is ambiguous and
after all not so appealing: for instance, something like destruct @1,
destruct #1, or destruct at 1, or destruct :(ind_pattern), meaning in
the latter case the first hypothesis whose type matches ind_pattern,
would have probably been better).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12355 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions