From de7d2fdb97975dcd94005bb6fa79a312c8afa017 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 28 Oct 2017 20:07:44 +0200
Subject: Fixing #5401 (printing of patterns with bound anonymous variables).

This fixes also #5731, #6035, #5364.
---
 test-suite/bugs/closed/5401.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/5401.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5401.v b/test-suite/bugs/closed/5401.v
new file mode 100644
index 0000000000..95193b993b
--- /dev/null
+++ b/test-suite/bugs/closed/5401.v
@@ -0,0 +1,21 @@
+(* Testing printing of bound unnamed variables in pattern printer *)
+
+Module A.
+Parameter P : nat -> Type.
+Parameter v : forall m, P m.
+Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
+Class U (R : P 0) (m : forall x, P x) : Prop.
+Instance w : U (f _ (fun _ => v _)) v.
+Print HintDb typeclass_instances.
+End A.
+
+(* #5731 *)
+
+Module B.
+Axiom rel : Type -> Prop.
+Axiom arrow_rel : forall {A1}, A1 -> rel A1.
+Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop.
+Axiom inl_rel: forall_rel _ (fun _ => arrow_rel).
+Hint Resolve inl_rel : foo.
+Print HintDb foo.
+End B.
-- 
cgit v1.2.3