test-suite/bugs/opened/3890.v


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.