blob: 1872dac10a6e9454a699142c49cf0d98cee476d9 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* Check that constraints on locals are preserved by discharging *)
Definition Type2 := Type.
Section A.
Local Type1 := Type : Type2.
Definition Type1' := Type1.
End A.
Definition Inconsistency := Type2 : Type1'.
|