The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Hi All,
  This would seem like a good opportunity to plead, once again and for 
the n-th time, for a
working model of coq-in-coq that works within the system. One would wish 
to be able to reflect
out of it (with a function) and into it (with a tactic). That way, 
Vladimir could write a function which
verifies on the coq-in-coq expression that it doesn't use his 
identifier; and also check by
reflecting back out that his expression is the same as what he thought 
it was.
Best,
---Carlos

Le 24/10/2014 15:07, Randy Pollack a écrit :
> Vladimir,
>
> If you want to prove some properties but not name the properties you
> can use "Goal" instead of "Lemma".
>
> Randy
>
>
> On Fri, Oct 24, 2014 at 6:47 AM, Vladimir Voevodsky 
> <vladimir AT ias.edu>
>  wrote:
> > Hello,
> >
> > is there a way to make sure that a certain identifier can not be used? The 
> > closest that I know to it is to make an identifier opaque but
> > I would like to make sure that an identifier is not used at all, e.g., I 
> > would like to say
> >
> > Hide identity_ind.
> >
> > and then if a tactic wants to use it it will generate an error.
> >
> > Vladimir.