coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] making a proof done with assert transparent

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] making a proof done with assert transparent
Date: Tue, 13 Oct 2015 09:39:37 +0200

On Tue, Oct 13, 2015 at 08:05:31AM +0200, Pierre-Marie Pédrot wrote:
> On 13/10/2015 05:58, Daniel de Rauglaudre wrote:
> > In the simple assert version these parentheses are not required.
>
> It ironically looks like a parsing engine issue... The "uconstr" entry
> is probably using a level smaller than the one of "*". If you want to
> overcome this issue introducing a new one, you can use the notation:

A parsing issue, mmm... who is the stupid guy who programmed the
system to parse Coq?

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
    - Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
      - RE: [Coq-Club] making a proof done with assert transparent, Soegtrop, Michael, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Jason Gross, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/13/2015
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Ilmārs Cīrulis, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015