The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Sorry, I forgot to change the topic name

Le Wed, 07 Apr 2010 19:55:59 +0200, AUGER 
<Cedric.Auger AT lri.fr>
 a écrit:

> Hi all, does anybody use coqdoc with multiple files?
> Before I upgrade my version (I don't remember which trunk it was),
> the (** printing ... ... *) commands were valid outside the file they  
> were:
>
> File A:
>
> (** printing X #Y# *)
>
> File B:
>
> Require Import A.
>
> (** [X] *)
>
> used to make an html file with "Y" printed.
>
> After an "svn up", it wasn't the case anymore...
> Can anybody tell me how to restore this feature?
>
> Le Wed, 07 Apr 2010 19:22:23 +0200, Vladimir Voevodsky  
> <vladimir AT ias.edu> a écrit:
>
> > You can use [set (a:= ....)].
> >
> > V.
> >
> >
> >
> > On Apr 6, 2010, at 6:25 AM, andré hirschowitz wrote:
> >
> > > Hello world,
> > >
> > > How can I pose a local definition within a proof
> > >
> > > writing something like
> > > pose (myname := ? : mytype)
> > >  instead of
> > > pose (myname := myformula )
> > >
> > > in such a way that
> > > -the next goal becomes mytype
> > > -so that myformula can be generated in proof mode
> > > ?
> > >
> > > Thanks for your attention.
> > >
> > > ah


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay