diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2016-08-14 00:32:26 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2016-08-14 00:32:26 +0200 |
| commit | 66ea13a2b855597ef8b5b648d0e8c398ac471933 (patch) | |
| tree | 242e116b8d5bf3a37820d9a877969c373949ddf9 | |
| parent | 01245b99b1d4b397ccfde65eeb59428f1d271539 (diff) | |
Replace "Set Implicit Arguments" option with "Set Printing Implicit".
Closes #99.
| -rw-r--r-- | coq/coq-abbrev.el | 4 | ||||
| -rw-r--r-- | coq/coq.el | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3f8662e7..4f2cf37a 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -190,8 +190,8 @@ It was constructed with `proof-defstringset-fn'.") ("OPTIONS" ["Set Printing All" coq-set-printing-all t] ["UnSet Printing All" coq-unset-printing-all t] - ["Set Implicit Argument" coq-set-implicit-arguments t] - ["Unset Implicit Argument" coq-unset-implicit-arguments t] + ["Set Printing Implicit" coq-set-printing-implicit t] + ["Unset Printing Implicit" coq-unset-printing-implicit t] ["Set Printing Width" coq-ask-adapt-printing-width-and-show t] ["Set Printing Synth" coq-set-printing-synth t] ["Unset Printing Synth" coq-unset-printing-synth t] @@ -1346,8 +1346,8 @@ goal is redisplayed." (proof-definvisible coq-show-proof "Show Proof.") (proof-definvisible coq-show-conjectures "Show Conjectures.") (proof-definvisible coq-show-intros "Show Intros.") ; see coq-insert-intros below -(proof-definvisible coq-set-implicit-arguments "Set Implicit Arguments.") -(proof-definvisible coq-unset-implicit-arguments "Unset Implicit Arguments.") +(proof-definvisible coq-set-printing-implicit "Set Printing Implicit.") +(proof-definvisible coq-unset-printing-implicit "Unset Printing Implicit.") (proof-definvisible coq-set-printing-all "Set Printing All.") (proof-definvisible coq-unset-printing-all "Unset Printing All.") (proof-definvisible coq-set-printing-synth "Set Printing Synth.") |