aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2750.v
blob: fc580f1018078cc9869d97d0c09a6e032d5e4f15 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

Module Type ModWithRecord.

  Record foo : Type :=
  { A : nat
  ; B : nat
  }.
End ModWithRecord.

Module Test_ModWithRecord (M : ModWithRecord).

  Definition test1 : M.foo :=
    {| M.A := 0
     ; M.B := 2
     |}.

  Module B := M.

  Definition test2 : M.foo :=
    {| M.A := 0
     ; M.B := 2
     |}.
End Test_ModWithRecord.