cpitclaudel/company-coq

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

zhengpushi opened this issue · 3 comments

zhengpushi commented

I think:
when typing "SPP", the tips list should contain "Set Printing Parentheses".
It's uesful for me to say.
Thanks for this great project!

cpitclaudel commented

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

txyyss commented

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 commented

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.