"SPP" for "Set Printing Parentheses" is useful, should be added.

[zhengpushi]

"SPP" for "Set Printing Parentheses" is useful, should be added.

[cpitclaudel]

Could you make a PR to add that command to the list?

[txyyss]

I would like to help because I have similar requests such as adding "Print Canonical Projections". I think such items should be added into company-coq--refman-vernac-abbrevs in company-coq-abbrev.el.

However, the list contains something I do not understand---the cdr part like ("g1" . 1094). What does it mean? If I know how to add such things properly, I would like make a PR with these changes. Thank you very much!

[cpitclaudel]

I think these are pointer to the docs (the outdated copy of them that company-coq ships with). But since we're not going to repackage the docs (yet), it's OK use a dummy value there.