From f6613489304a30846af28334c040c7d4f9e4addc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 8 Jan 2019 15:57:27 +0100
Subject: Restrict universes in records.

Fix #8076.
---
 test-suite/bugs/closed/bug_8076.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8076.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_8076.v b/test-suite/bugs/closed/bug_8076.v
new file mode 100644
index 0000000000..7bee43620f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8076.v
@@ -0,0 +1,3 @@
+
+Notation leak a := ltac:(let x := constr:(Type) in exact a) (only parsing).
+Record foo@{} (P:leak Prop) := { f : leak Prop }.
-- 
cgit v1.2.3