diff options
| author | Hugo Herbelin | 2020-11-22 11:28:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 11:28:06 +0100 |
| commit | f5ccc82ce8f2db919b288f3a853dbf238615de59 (patch) | |
| tree | fc2151e909aac796f7ddc0ebdd4b6b0029a527d0 /test-suite/bugs | |
| parent | 9c841105fe2b51305abcba7bd8a574705dbd1adf (diff) | |
Fixes another instance of bug #7967: restriction of universes in "Context".
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_7967.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v index 2c8855fd54..987a820831 100644 --- a/test-suite/bugs/closed/bug_7967.v +++ b/test-suite/bugs/closed/bug_7967.v @@ -1,2 +1,6 @@ Set Universe Polymorphism. Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. + +(* A similar bug *) +Context (C := ltac:(let y := constr:(Type) in exact nat)). +Check C@{}. |