diff options
| -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.") |