blob: da0cc68a4ea29f775a6dad52030bcb596a69a1b7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Testing consistency of globalization and interpretation in some
extreme cases *)
Section sect.
(* Simplification of the initial example *)
Hypothesis Other: True.
Lemma C2 : True.
proof.
Fail have True using Other.
Abort.
(* Variant of the same problem *)
Lemma C2 : True.
Fail clear; Other.
Abort.
|
