test-suite/bugs/closed/bug_13249.v


1
2
3
4
5
6
7
8
9

Global Generalizable All Variables.

Section test.
  Context {A : Type}.
  Context `{!foo A}.

  Goal foo A.
  Proof. assumption. Defined.
End test.