The Coq mailing list

[Abhishek Kr Singh <abhishek.uor AT gmail.com>]

Dear Michael,

Thanks for pointing out.

 Indeed, there is a Coercion is_true which maps bool to Prop.  I have changed the Ltac definition as 

 Ltac show_H:=

    match goal with

    | H: is_true (?x == ?y)%bool |- _ =>  idtac H

    end.

and it worked correctly. Thanks again.

On Thu, Aug 16, 2018 at 4:10 PM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Abishek,

 

I guess you have a coercion defined from bool to Prop, otherwise eqb x y cannot be on the left side of -> .

 

Ltac doesn’t know about this coercion, so I think you have to put in the coercion from bool to Prop explicitly in your Ltac match. Enable “Display Coercions” to see what your goal really is.

 

I also would use an explicit type scope (?x == ?y)%bool for clarity.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

--

Thanks and Regards.

Abhishek Kr. Singh,
Research Scholar, STCS, TIFR Mumbai.
Homepage:  http://www.tcs.tifr.res.in/~abhishek/

 http://www.tcs.tifr.res.in/people/abhishek-singh