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
