diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 14:24:01 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 14:24:01 +0100 |
| commit | 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d (patch) | |
| tree | c3703906dfa0b1d3c43380afa477dd62859da916 | |
| parent | e99e4006368fab3818812c6194d54465746c4566 (diff) | |
Update test for #3363 now that Require is forbidden inside modules.
| -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. |