diff options
| author | Pierre-Marie Pédrot | 2021-03-19 14:10:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-19 14:10:07 +0100 |
| commit | 1e28f86f1947142095e18f4fdd11ed036e7a6e33 (patch) | |
| tree | 048bc2b37ed3cd247778936fbcb846b840f4c80e /test-suite | |
| parent | be64fe07ec2bcf5177bb227813d8f896ef00c265 (diff) | |
| parent | 2a07fb44bd453fe9ff2649b498dfb6c0e8001324 (diff) | |
Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transitively closed
Reviewed-by: ppedrot
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. |