From ce1d51dc40cdb65b01b559ab076f76b265ccf6c4 Mon Sep 17 00:00:00 2001 From: Gaƫtan Gilbert Date: Sun, 13 Oct 2019 20:20:56 +0200 Subject: Fix #10888: Context import behaviour in modtype --- test-suite/bugs/closed/bug_10888.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/bug_10888.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v new file mode 100644 index 0000000000..3c2e8011d7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10888.v @@ -0,0 +1,11 @@ + +Module Type T. +Context {A:Type}. +End T. + +Module M(X:T). + Import X. + Check X.A. + Check A. + Definition B := A. +End M. -- cgit v1.2.3