The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

You mean the error gotten by reverting 
a7ea32fbf3829d1ce39ce9cc24b71791727090c5 is in this case better?

Gaëtan Gilbert

On 24/06/2017 16:55, Emilio Jesús Gallego Arias wrote:
> 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.