From 66ea13a2b855597ef8b5b648d0e8c398ac471933 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 14 Aug 2016 00:32:26 +0200
Subject: Replace "Set Implicit Arguments" option with "Set Printing Implicit".

Closes #99.
---
 coq/coq-abbrev.el | 4 ++--
 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]
diff --git a/coq/coq.el b/coq/coq.el
index afb5f35a..59f3fb04 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.")
-- 
cgit v1.2.3