Parameters in pattern first step.

In interp/constrintern.ml, '_' for constructor parameter are required if you use
AppExpl ('@Constr') and added in order to be erased at the last time if you do not
use '@'.

It makes the use of notation in pattern more permissive. For example,
-8<------
Inductive I (A: Type) : Type := C : A -> I A.

Notation "x <: T" := (C T x) (at level 38).

Definition uncast A (x : I A) :=
match x with
 | x <: _ => x
end.
-8<------
was forbidden.

Backward compatibility is strictly preserved expect for syntactic definitions:
While defining "Notation SOME = @Some", SOME had a special treatment and used to
be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be
provided for parameters).

In interp/constrextern.ml, except if all the parameters are implicit and all the
arguments explicit (This covers all the cases of the test-suite), pattern are
generated with AppExpl (id est '@') (so with '_' for parameters) in order to
become compatible in any case with future behavior.

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

0 files changed, 0 insertions, 0 deletions