The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Oct 29, 2008 at 03:59:28PM +0000, Thorsten Altenkirch wrote:
> Thank you & Laurent & Georges (in private) for you helpful comments.
> 
> I guess I was looking for something like
> 
> Reset Initial "-nois"
> 
> available as a vernacular command. But this doesn't seem to exist.
> 

Well, from inside Coq, you can actually emulate this "-nois" option,
thanks to the old commands Write State and Restore State. All you need
is to manage to launch coqtop or coqide once with the -nois option,
and save this empty state via: "Write State empty". This should create
a file named empty.coq. Later on, from any usual coq session, a
"Restore State empty" will bring you back to this empty environment.

Best regards,

Pierre L.