coq-mode inhibits automatic saving of abbrevs

[coquser]

Setting save-abbrevs to nil in coq-install-abbrevs disables automatics saving of any abbreviation that the user defined in this emacs session. This is not acceptable for people who do use abbrevs.

[courtieu]

This is fixed in cvs. Thanks for reporting. I removed the setting of save-abbrev (this was bad).

Problem: I don't know how to set abbreviation save mode for coq: the behaviour I want is: if the user sets some coq abbreviation by himself, then he knows what he is doing and we should not interfere with save-abbrev. Otherwise never save coq abbrevs so that standard abbrev can be updated when proofgeneral is updated. Maybe having standard abbreviations in coq mode is bad practice at all.

Insights welcome.

[David Aspinall]

I suppose Coq might just have a setting which is "Manage abbrevs for Coq" in which you take control of abbrevs, and try to set the default of that setting by seeing if the user has a saved abbrev file with the standard file name.

Or maybe you just have an operation which is "Update abbrevs for Coq" which modifies the table with PG's entries. The user has to learn to save if they want to and otherwise use that command.

Personally I gave up using abbrevs some years ago because I couldn't keep my tables in sync across multiple computers and (shock horror) increasingly often was editing things outside Emacs.