diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:09:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:51:02 +0200 |
| commit | fd0cd480a720cbba15de86bbc9cad74ba6d89675 (patch) | |
| tree | 157da3e6f8a88f752fe516e34d70d58a7864021c /test-suite/bugs/closed/4932.v | |
| parent | 2042daa9a6e13cbb9636a62812015749d95c2283 (diff) | |
A new step on using alpha-conversion in printing notations.
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
Diffstat (limited to 'test-suite/bugs/closed/4932.v')
| -rw-r--r-- | test-suite/bugs/closed/4932.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v index df200cdce..219d532ac 100644 --- a/test-suite/bugs/closed/4932.v +++ b/test-suite/bugs/closed/4932.v @@ -28,13 +28,17 @@ Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt)) (existT _ (y,z) tt). Example test := tele (t : Type) := tt. -Check test nat. +Example test' := test nat. +Print test. Example test2 := tele (t : Type) (x:t) := tt. -Check test2 nat 0. +Example test2' := test2 nat 0. +Print test2. -Check tele (t : Type) (y:=0) (x:t) := tt. -Check (tele (t : Type) (y:=0) (x:t) := tt) nat 0. +Example test3 := tele (t : Type) (y:=0) (x:t) := tt. +Example test3' := test3 nat 0. +Print test3. -Check tele (t : Type) '((y,z):nat*nat) (x:t) := tt. -Check (tele (t : Type) '((y,z):nat*nat) (x:t) := tt) nat (1,2) 3. +Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Example test4' := test4 nat (1,2) 3. +Print test4. |