The Coq mailing list

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

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