blob: c7926711938de83d7d37d2abab810cd595844364 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* 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}.
|
