coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewrite does not work

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr, Marcus Ramos <marcus.ramos AT univasf.edu.br>
Subject: Re: [Coq-Club] Rewrite does not work
Date: Mon, 28 Jul 2014 06:38:51 +0200

On 27/07/2014 22:33, AUGER Cédric wrote:
> What would be nice with Coq reporting error is the following behavior:
> if there is a subterm which is printed exactly like the one reported in
> the error, then reprint the hypothesis and the error with display of
> implicit arguments.

This should already be the case in trunk, and consequently this feature
will be there in 8.5.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Rewrite does not work, Marcus Ramos, 07/27/2014
- Re: [Coq-Club] Rewrite does not work, Jonathan, 07/27/2014
- Re: [Coq-Club] Rewrite does not work, AUGER Cédric, 07/27/2014
  - Re: [Coq-Club] Rewrite does not work, Jonathan, 07/27/2014
  - Re: [Coq-Club] Rewrite does not work, Pierre-Marie Pédrot, 07/28/2014
  - Re: [Coq-Club] Rewrite does not work, Marcus Ramos, 07/29/2014
    - Re: [Coq-Club] Rewrite does not work, Cedric Auger, 07/29/2014
      - Re: [Coq-Club] Rewrite does not work, Enrico Tassi, 07/29/2014
        
        Re: [Coq-Club] Rewrite does not work, Xavier Leroy, 07/30/2014
        
        Re: [Coq-Club] Rewrite does not work, Jonathan, 07/30/2014
        
        Re: [Coq-Club] Rewrite does not work, Xavier Leroy, 07/31/2014
        Re: [Coq-Club] Rewrite does not work, Jonathan, 07/31/2014
        Re: [Coq-Club] Rewrite does not work, Jason Gross, 07/31/2014
        Re: [Coq-Club] Rewrite does not work, Jonathan, 07/31/2014
        
        Re: [Coq-Club] Rewrite does not work, Randy Pollack, 07/31/2014