From 9f91b1072d5fe1da6fb7ab525ec44e9e8621a7e2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 14 Mar 2000 10:58:03 +0000 Subject: Note about useless output from Coq --- coq/todo | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/coq/todo b/coq/todo index 61b9f612..5781026e 100644 --- a/coq/todo +++ b/coq/todo @@ -4,6 +4,24 @@ See also ../todo for generic things to do, priority codes. + +** B See if there is a way to turn off the superfluous output of scripts + + from Coq when inside ProofGeneral, i.e. output like this: + + Intros A B G. + Induction G. + Apply conj. + Assumption. + + Assumption. + + and_comms is defined + + In PG, only the last line is relevant!! + If it isn't possible to turn it off, can we send a suggestion + to the Coq implementors for the next version? + ** B Fix silly startup sychronization problem that displays cwd on startup. -- cgit v1.2.3