blob: 804ba1d3785ce9da6a2a7f005e00d94bbabd48f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* #7329 *)
Set Primitive Projections.
Module M.
Module Bar.
Record Box := box { unbox : Type }.
Axiom foo : Box.
Axiom baz : forall _ : unbox foo, unbox foo.
End Bar.
End M.
Include M.
|