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
> 

Attachment: 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

Reply via email to