aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/4813.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/opened/4813.v')
-rw-r--r--test-suite/bugs/opened/4813.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
new file mode 100644
index 000000000..b75170179
--- /dev/null
+++ b/test-suite/bugs/opened/4813.v
@@ -0,0 +1,5 @@
+(* An example one would like to see succeeding *)
+
+Record T := BT { t : Set }.
+Record U (x : T) := BU { u : t x -> Prop }.
+Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.