aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/import_mod.v
blob: c098c6e890f50cf1c3b16d956eab2fe8979d75f8 (plain)
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

Definition p := 0.
Definition m := 0.

Module Test_Import.
  Module P.
    Definition p := 1.
  End P.

  Module M.
    Import P.
    Definition m := p.
  End M.

  Module N.
    Import M.

    Lemma th0 : p = 0.
      reflexivity.
    Qed.

  End N.


  (* M and P should be closed *)
  Lemma th1 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.


  Import N.

  (* M and P should still be closed *)
  Lemma th2 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.
End Test_Import.


(********************************************************************)


Module Test_Export.
  Module P.
    Definition p := 1.
  End P.

  Module M.
    Export P.
    Definition m := p.
  End M.

  Module N.
    Export M.

    Lemma th0 : p = 1.
      reflexivity.
    Qed.

  End N.


  (* M and P should be closed *)
  Lemma th1 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.


  Import N.

  (* M and P should now be opened *)
  Lemma th2 : m = 1 /\ p = 1.
    split; reflexivity.
  Qed.
End Test_Export.