summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/HoTT_coq_052.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_052.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_052.v22
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_052.v b/test-suite/bugs/closed/HoTT_coq_052.v
new file mode 100644
index 00000000..62bb9fa1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_052.v
@@ -0,0 +1,22 @@
+Goal Type = Type.
+ Fail match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Prop.
+ Fail match goal with |- Type => idtac end.
+Abort.
+
+Goal Prop = Set.
+ (* This should fail *)
+ Fail match goal with |- ?x = ?x => idtac x end.
+Abort.
+
+Goal Type = Prop.
+ (* This should fail *)
+ Fail match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Type = Set.
+ (* This should fail *)
+ Fail match goal with |- ?x = ?x => idtac end.
+Abort.