aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive/4289.v
blob: 610a509c9b243736d8bc0a771b69b0c1c8e107c5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(* Checking backtracking with modules which used to fail due to an
   hash-consing bug *)

Module Type A.
  Axiom B : nat.
End A.
Module C (a : A).
  Include a.
  Definition c : nat := B.
End C.
Back 4.
Module C (a : A).
  Include a.
  Definition c : nat := B.