diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 18:54:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 20:30:11 +0200 |
| commit | 5d3d60e88f137183b4155bfa446dc7f3ebb35993 (patch) | |
| tree | 47b14bce769ce243310173d8abf8033619d34592 /test-suite | |
| parent | a267b06c4a237ce3e4ce257e47f6429543804baa (diff) | |
Fixing a bug of recursive notations introduced in dfdaf4de.
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e5dbfcb4b..65efe228a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -122,3 +122,5 @@ return (1, 2, 3, 4) : nat * nat * nat * nat {{ 1 | 1 // 1 }} : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b1015137d..ea372ad1a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4). Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. + +(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) +Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). +Check !!! (x y:nat), True. |