diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-16 10:10:43 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-16 10:10:43 +0000 |
commit | bc37c572cae76b6365f86eb5ebc05905b78577cf (patch) | |
tree | c23e2244d8c5a43969c2387c055888427678390b /test-suite | |
parent | 42a1588c7b1d38df5192c80b62b32dbafce07d55 (diff) |
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
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/Cases.out | 7 | ||||
-rw-r--r-- | test-suite/output/Cases.v | 12 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations.v | 2 |
4 files changed, 22 insertions, 3 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 1ec02c56a..c99e03276 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -27,5 +27,12 @@ fix foo (A : Type) (l : list A) {struct l} : option A := : forall A : Type, list A -> option A Argument scopes are [type_scope list_scope] +uncast = +fun (A : Type) (x : I A) => match x with + | x0 <: _ => x0 + end + : forall A : Type, I A -> A + +Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index b63375867..505418b14 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -34,6 +34,18 @@ Fixpoint foo (A:Type) (l:list A) : option A := Print foo. +(* Accept and use notation with binded parameters *) + +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. + +Print uncast. + (* Do not duplicate the matched term *) Axiom A : nat -> bool. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index ada524f1c..5a32cff96 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -116,8 +116,8 @@ fun x : option Z => match x with end : option Z -> Z fun x : option Z => match x with - | SOME3 x0 => x0 - | NONE3 => 0 + | SOME3 _ x0 => x0 + | NONE3 _ => 0 end : option Z -> Z s diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 4a2c411ee..e560aecd8 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -244,7 +244,7 @@ Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. Notation SOME3 := @Some. -Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). +Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). (* Check correct matching of "Type" in notations. Of course the notation denotes a term that will be reinterpreted with a different |