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.
|
