coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Ltac: Matching on hypothesis which contains user defined notations

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Ltac: Matching on hypothesis which contains user defined notations
Date: Thu, 16 Aug 2018 10:40:01 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:n1anKxbeIpHHtPQ9kAUw3xv/LSx+4OfEezUN459isYplN5qZr8m6bnLW6fgltlLVR4KTs6sC17KI9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa8bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbb46OOfVkYq/QeckXSXZdUstTUSFKH4Oyb5EID+oEJetUoZTzp1wQohuxGQmsHuTvyidQinTr2qM60vguEQHc0wM+G9ICvmnfodLwNKcTTe+1zLPHwivHb/9Mwjf975bHch89ofGWWrJwadHcyUgpFwPZkFqQrZbpMC+S1uQIqmWW6fdrW+yoi24isQ5xoz6vy98tionPmoIa1FTE+T9kz4krI9CzVU11Yca8HZdNuSyXOJF6Tt4sTmxnoio217MLtJ+hcCQU1Jgr3wPTZv2JfoSS7B/uWvydLSl2iX9hYr6zmhW//Va4xuHhV8S51ExGojRFn9TDrHwByQbf5tWER/dh+EqqxCyB2BrJ6u5eJEA5jarbJIAlwr43jpcTtEvDETXqlEnolqOWd0Mk+vS25OTjeLnpupicN4pshgH/NKQhhNC/DPwlPgUAUGWX4/mw2bPs8EHjXblHgPw7nrPHvJzGPcgbo7S2Aw5R0oYt8Ra/CDKm3cwdnXkGMF1FeAiIgJbtO13UO/D4Cumwg1uwkDdxwPDGJqbsApTLLnjfjrjheaxx5FJbyAo21dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zBUWerDs1p8KYli5GO5nKgOXezCk1twGCCIBuhc0ZO3sklyLFzBJMSWcRaU5s3sAD4+pEZ3EXsTlpb2K3C62GtceMmVHAVCFHHOubIKJVOsWbzq6I8l9nzhCXr+kHdxynSqyvRP3nuI0ZtHf/TcV4Mq6hYpFotbLnBR3zgRaSsGU0mWDVWZxxzpaRjkq0aQ5qkt4mA7ajfpIxsdAHNkW3MtnFx8gPMeFne18F932HAnGe4XREQv0cpCdGTg0C+kJ7ZoObkJ6Qorwix/Kh3DsArkJmrjND5sxoPrR

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

[Coq-Club] Ltac: Matching on hypothesis which contains user defined notations, Abhishek Kr Singh, 08/16/2018
- RE: [Coq-Club] Ltac: Matching on hypothesis which contains user defined notations, Soegtrop, Michael, 08/16/2018
  - Re: [Coq-Club] Ltac: Matching on hypothesis which contains user defined notations, Abhishek Kr Singh, 08/16/2018