yes: there's a user-facing option called coq-search-blacklist-string. It's set to the same defaults as Coq, but if you change it these calls will look different.
On 2016-05-26 13:43, Paul A. Steckler wrote: > 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 >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
