diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 17 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index e8e206791..975e2ffdf 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -14,6 +14,12 @@ forall n : nat, n = 0 : Prop !(0 = 0) : Prop +forall n : nat, #(n = n) + : Prop +forall n n0 : nat, ##(n = n0) + : Prop +forall n n0 : nat, ###(n = n0) + : Prop 3 + 3 : Z 3 + 3 diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 93ccf7a8c..1d24e70a1 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -28,6 +28,23 @@ Check forall n:nat, 0=0. End A. (**********************************************************************) +(* Behaviour wrt to binding variables (cf bug report #1186) *) + +Section B. + +Notation "# A" := (forall n:nat, n=n->A) (at level 60). +Check forall n:nat, # (n=n). + +Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60). +Check forall n n0:nat, ## (n=n0). + +Notation "### A" := + (forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60). +Check forall n n0:nat, ### (n=n0). + +End B. + +(**********************************************************************) (* Conflict between notation and notation below coercions *) (* Case of a printer conflict *) |