The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Gaetan Gilbert 
<gaetan.gilbert AT ens-lyon.fr>
 writes:

> Why is the error
>
> Error:
> The term "Bool.eqb_prop" has type
>  "forall (a b : bool) (_ : @eq bool (Bool.eqb a b) true), @eq bool a b"
> while it is expected to have type
>  "forall (x y : bool) (_ : @eq bool (@eqb bool ?e x y) true), @eq bool
> x y".
>
> though? I don't see a nat in there.

Gaëtan, this is likely due to the use of the wrong evar map in

let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =

if you change:

            error_actual_type ?loc env best_failed_evd cj t e
to
            error_actual_type ?loc env _evd cj t e

in the "saturate_evd" case (the responsible of triggering TC resolution
here) you should see the right error message.

I think this is a bug indeed.

E.