blob: fbe5e20f2fdff616b5120a8fdafc6fdf140a3dd3 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Error message was not printed in the correct environment *)
Fail Parameters (A:Prop) (a:A A).
(* This is a variant (reported as part of bug #2347) *)
Require Import EquivDec.
Fail Program Instance bool_eq_eqdec : EqDec bool eq :=
{equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
|
