aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2640.v
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.