diff options
| -rw-r--r-- | test-suite/bugs/opened/3363.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v index 8307fdf506..800d89573c 100644 --- a/test-suite/bugs/opened/3363.v +++ b/test-suite/bugs/opened/3363.v @@ -1,4 +1,19 @@ -(** In this file, either both [Check]s should fail, or both should succeed. *) +(** In this file, either all four [Check]s should fail, or all four should succeed. *) +Module A. + Section HexStrings. + Require Import String. + End HexStrings. + Fail Check string. +End A. + +Module B. + Section HexStrings. + Require String. + Import String. + End HexStrings. + Fail Check string. +End B. + Section HexStrings. Require String. Import String. |