aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-22 18:12:36 +0200
committerHugo Herbelin2019-05-22 18:12:36 +0200
commit5c5bd952e9c28c3acf740fcdced03b2b7145076d (patch)
treea56647f099136d571f2f2c6c47ddb31472ef7804 /test-suite
parent4f2e05f5abc19addc25501281b4cd34ed5e33853 (diff)
parent28dfb113c19f467fdc2b785d1c5a07a42aefa488 (diff)
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalization + cleanups
Reviewed-by: herbelin
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_10176.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10176.v b/test-suite/bugs/closed/bug_10176.v
new file mode 100644
index 0000000000..fdb0eb87a4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10176.v
@@ -0,0 +1,7 @@
+Class Foo (xxx:nat) := foo : nat.
+
+Lemma aa `{Foo} : nat. Abort.
+
+Fail Lemma xy (Foo:bool->Type) `{Foo} : nat.
+
+Fail Lemma yx (Fooo:bool->Type) `{Fooo} : nat.