diff options
| -rw-r--r-- | test-suite/bugs/opened/3397.v | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/test-suite/bugs/opened/3397.v b/test-suite/bugs/opened/3397.v deleted file mode 100644 index f5d406d3a8..0000000000 --- a/test-suite/bugs/opened/3397.v +++ /dev/null @@ -1,24 +0,0 @@ -Set Printing All. -Typeclasses eauto := debug. -Module success. - Class foo := { F : nat }. - Class bar := { B : nat }. - Instance: foo := { F := 1 }. - Instance: foo := { F := 0 }. - Instance: bar := { B := 0 }. - Definition BAZ := eq_refl : @F _ = @B _. -End success. - -Module failure. - Class foo := { F : nat }. - Class bar := { B : nat }. - Instance f0: foo := { F := 0 }. - Instance f1: foo := { F := 1 }. - Instance b0: bar := { B := 0 }. - Fail Definition BAZ := eq_refl : @F _ = @B _. - (* Toplevel input, characters 18-25: -Error: -The term "@eq_refl nat (@F f1)" has type "@eq nat (@F f1) (@F f1)" -while it is expected to have type "@eq nat (@F f1) (@B b0)" -(cannot unify "@F f1" and "@B b0"). *) -End failure. |