diff options
| author | sacerdot | 2004-04-01 15:07:57 +0000 |
|---|---|---|
| committer | sacerdot | 2004-04-01 15:07:57 +0000 |
| commit | b4031e79051e9efd78ad915382235a5be19e50a2 (patch) | |
| tree | 7e0e538b31d6a3db801d3b9b78fc1452de44a8f1 /dev/base_include | |
| parent | c8002490d96fbc6903c13617dfbdff1dd599b78c (diff) | |
Output of theory files reimplemented using Buffer.
This avoids stdout cluttering in interactive mode.
Whenever verbose is set to true, all the strings sent to
the Buffer are also printed on stdoud.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5628 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions