aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-01-22 14:52:38 +0100
committerPierre-Marie Pédrot2020-01-22 14:52:38 +0100
commitdc25c63771fb32a4236b04eb940e7881f28669e1 (patch)
treedc33334717fd6717036c2f716115820878a75d12 /test-suite
parent2c71d636f80327500ea75c1c1ce59c554001a078 (diff)
parent71aa415282a93a6e23af3b824f8531c58d2d66bd (diff)
Merge PR #11422: Fix #11421 computation of Set+2
Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_11421.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v
new file mode 100644
index 0000000000..8ddf05c888
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11421.v
@@ -0,0 +1 @@
+Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}.