coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] local definition in proof mode

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>
Cc: AUGER <Cedric.Auger AT lri.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] local definition in proof mode
Date: Wed, 7 Apr 2010 17:03:07 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=rLiLoRB/A7RwEiRYsi0sPsCizDAQeDooLYSchWIofOqiOtPr/21Tiae7P+pYrfGLpG 4FXoWLKkYsCgcOQ1niaCrE3Jlp9Fm0JF9o3a1f1ehtZ+iZHU/zXA2e6AWNmIPRnvYIj+ BneiEemF/J8NUCe7QlPZ4UuKsRMflbXPDbzf8=

Yes that's right. You can only see its definition but you cannot make
it transparent.
P.

Le 7 avril 2010 15:51, Pierre-Marie P�drot
<pierremarie.pedrot AT ens-lyon.fr>
a �crit :
> Technically, it does not work as the term produced through abstract is
> opaque, so we end up with the very same problem as assert.
>
> PMP

Re: [Coq-Club] local definition in proof mode, (continued)
- Re: [Coq-Club] local definition in proof mode, Vladimir Voevodsky
  - Re: [Coq-Club] local definition in proof mode, AUGER
    - [Coq-Club] [Coq-club] problems with Coqdoc, AUGER