From 0daae2bd1ab518d8fcb6d59a5616786ade94d1e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 22 Dec 2017 16:26:24 +0100
Subject: Deprecate implicit tactic solving.

---
 theories/Logic/Diaconescu.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 3317766c9..66e82ddbf 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -234,8 +234,6 @@ Qed.
 (** An alternative more concise proof can be done by directly using
     the guarded relational choice *)
 
-Declare Implicit Tactic auto.
-
 Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
 Proof.
   assert (decide: forall x:A, x=a1 \/ x=a2 ->
-- 
cgit v1.2.3