The Coq mailing list

[Georg Neis <neis AT mpi-sws.org>]

Hi,

I'm wondering if the following behaviour is intended.


File main.v:
------------
Global Set Printing All.
Check 1.  (* prints "S O" *)
Require a.
Check 1.  (* prints "1" *)

File a.v:
---------
Global Unset Printing All.
Require b.

File b.v:
---------
Global Set Printing All.


I would have expected the second check to print "S O", just like the
first did.  I have played around with using Require Import/Export
instead of just Require, but the behaviour stays the same.

Best,
 Georg