diff options
| author | Gaëtan Gilbert | 2021-03-10 17:06:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-03-10 17:06:22 +0100 |
| commit | 2a07fb44bd453fe9ff2649b498dfb6c0e8001324 (patch) | |
| tree | d9b5030c56f12d1da6f88416883d7191803005a1 /test-suite | |
| parent | cde4dceb93ba1f91d20f13a0fdea8f9731a6a626 (diff) | |
Fix kernel incorrectly assuming the "using" hyps are transitively closed
Fix #13903
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13903.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13903.v b/test-suite/bugs/closed/bug_13903.v new file mode 100644 index 0000000000..7c1820b85c --- /dev/null +++ b/test-suite/bugs/closed/bug_13903.v @@ -0,0 +1,5 @@ +Section test. +Variables (T : Type) (x : T). +#[using="x"] Definition test : unit := tt. +End test. +Check test : forall T, T -> unit. |