diff options
| -rw-r--r-- | test-suite/bugs/opened/3363.v | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v index 800d89573..8307fdf50 100644 --- a/test-suite/bugs/opened/3363.v +++ b/test-suite/bugs/opened/3363.v @@ -1,19 +1,4 @@ -(** 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. - +(** In this file, either both [Check]s should fail, or both should succeed. *) Section HexStrings. Require String. Import String. |