aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2388.v
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}.