When Proof General starts coqtop, it issues this sequence of commands:
--
Add Search Blacklist "Private_" "_subproof".
Set Printing Depth 50 .
Remove Search Blacklist "Private_" "_subproof".
Add Search Blacklist "Private_" "_subproof".
--
The Remove/Add are issued from a single PG-internal call to reset the
search blacklist. But that call seems redundant, given the initial
Add.

Is there a justification for this sequence of commands?

-- Paul
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to