coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with terms differing in their obligations

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Adam Koprowski <adam.koprowski AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Problem with terms differing in their obligations
Date: Mon, 1 Mar 2010 22:37:24 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=c2z/2L2dX9FMYn0hfGdGEluASnRYm6ZArBYuWIhXhVmc9J+/mUi4t03doKFRsMQPAu uPdntxvBifIOD6x20BoukjCO3EHOSOKYg4m299MXF07eaMoKHTjDE0mtJoR4KD1Z1WY/ lp7snRrkYr1ngAfyY9DOK08IXc0jkyxReZONw=

Thanks, but how do I actually tell coq to apply it to the right places?

I'd rather not have to write out
� �assert (EnlargeTransitiveCommuteRelation2_obligation_4 ... =
� � � � � �EnlargeTransitiveCommuteRelation2_obligation_1 ...).
� � � �apply proof_irrelevance.
etc. if I can get away without it.

��You should be able to write custom Ltac macros that will do that for you.�

��Best,

��Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[Coq-Club] Problem with terms differing in their obligations, Ian Lynagh
- Re: [Coq-Club] Problem with terms differing in their obligations, Adam Koprowski
  - Re: [Coq-Club] Problem with terms differing in their obligations, Ian Lynagh
    - Re: [Coq-Club] Problem with terms differing in their obligations, Adam Koprowski
      - Re: [Coq-Club] Problem with terms differing in their obligations, Matthieu Sozeau