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

Is there a justification for this sequence of commands?

-- Paul
ProofGeneral-devel mailing list

Reply via email to