test-suite/bugs/opened/3363.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

(** 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.
End HexStrings.
Fail Check string.

Section HexStrings'.
  Require Import String.
End HexStrings'.
Check string.