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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
(* Bug report #3746 : Include and restricted signature *)
Module Type MT. Parameter p : nat. End MT.
Module Type EMPTY. End EMPTY.
Module Empty. End Empty.
(* Include of an applied functor with restricted sig :
Used to create axioms (bug report #3746), now forbidden. *)
Module F (X:EMPTY) : MT.
Definition p := 0.
End F.
Module InclFunctRestr.
Fail Include F(Empty).
End InclFunctRestr.
(* A few variants (indirect restricted signature), also forbidden. *)
Module F1 := F.
Module F2 (X:EMPTY) := F X.
Module F3a (X:EMPTY). Definition p := 0. End F3a.
Module F3 (X:EMPTY) : MT := F3a X.
Module InclFunctRestrBis.
Fail Include F1(Empty).
Fail Include F2(Empty).
Fail Include F3(Empty).
End InclFunctRestrBis.
(* Recommended workaround: manual instance before the include. *)
Module InclWorkaround.
Module Temp := F(Empty).
Include Temp.
End InclWorkaround.
Compute InclWorkaround.p.
Print InclWorkaround.p.
Print Assumptions InclWorkaround.p. (* Closed under the global context *)
(* Related situations which are ok, just to check *)
(* A) Include of non-functor with restricted signature :
creates a proxy to initial stuff *)
Module M : MT.
Definition p := 0.
End M.
Module InclNonFunct.
Include M.
End InclNonFunct.
Definition check : InclNonFunct.p = M.p := eq_refl.
Print Assumptions InclNonFunct.p. (* Closed *)
(* B) Include of a module type with opaque content:
The opaque content is "copy-pasted". *)
Module Type SigOpaque.
Definition p : nat. Proof. exact 0. Qed.
End SigOpaque.
Module InclSigOpaque.
Include SigOpaque.
End InclSigOpaque.
Compute InclSigOpaque.p.
Print InclSigOpaque.p.
Print Assumptions InclSigOpaque.p. (* Closed *)
(* C) Include of an applied functor with opaque proofs :
opaque proof "copy-pasted" (and substituted). *)
Module F' (X:EMPTY).
Definition p : nat. Proof. exact 0. Qed.
End F'.
Module InclFunctOpa.
Include F'(Empty).
End InclFunctOpa.
Compute InclFunctOpa.p.
Print InclFunctOpa.p.
Print Assumptions InclFunctOpa.p. (* Closed *)
|
