From fd0cd480a720cbba15de86bbc9cad74ba6d89675 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Jul 2016 15:09:08 +0200
Subject: 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).
---
 test-suite/bugs/closed/4932.v | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v
index df200cdce0..219d532ac6 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.
-- 
cgit v1.2.3