aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3289.v
blob: 4542b015d0432c007d50f0543a0fec125dbfc328 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *)

Class Contr_internal (A : Type) :=
  BuildContr { center : A ;
               contr : (forall y : A, True) }.
Class Contr A := Contr_is_contr : Contr_internal A.
Inductive Unit : Set := tt.
Instance contr_unit : Contr Unit | 0 :=
  let x := {|
        center := tt;
        contr := fun t : Unit => I
      |} in x. (* success *)

Instance contr_internal_unit' : Contr_internal Unit | 0 :=
  {|
    center := tt;
    contr := fun t : Unit => I
  |}.

Instance contr_unit' : Contr Unit | 0 :=
  {|
    center := tt;
    contr := fun t : Unit => I
  |}.
(* Error: Mismatched contexts while declaring instance:
 Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1)
 Found:   tt  (fun t : Unit => I) *)