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
