Introduced in f77c366, one can use Feedback.set_trace "TheoryPP.include_docs" 0 to exclude the theorem list from the generated .sig file. This issue is about adding syntactic sugar using a new tag (no_sig_docs) for the Theory syntax.

For example:

Theory foo[no_sig_docs] 

should result in the generated export_theory call to look something like

Feedback.set_trace "TheoryPP.include_docs" 0 before Theory.export_theory()

In other words, with the tag no_sig_docs, unquote should add Feedback.set_trace "TheoryPP.include_docs" 0 before as a prefix to the export_theory call.