aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3890.v
blob: f9ac9be2c8c8002b8ba3d449e2daae34097cbc0a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Class Foo.
Class Bar := b : Type.

Instance foo : Foo := _.
(* 1 subgoals, subgoal 1 (ID 4)
  
  ============================
   Foo *)

Instance bar : Bar.
exact Type.
Defined.
(* bar is defined *)

About foo.
(* foo not a defined object. *)

Fail Defined.