From d08282cb2242d642d8ea40e844dbe61b7404674c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 22 May 2012 12:09:18 +0000
Subject: SetoidList: explicit the fact that InfA_compat won't use ltA_strorder

 For that, we use the new "Proof using ...". This way, we're sure
 that a later change in the behavior of intuition or any other tactics
 will not create an artificial dependency again (cf. r15180).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/SetoidList.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 6c573a1271..f6eab86496 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -647,7 +647,7 @@ Proof.
 Qed.
 
 Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
-Proof.
+Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *)
  intros x x' Hxx' l l' Hll'.
  inversion_clear Hll'.
  intuition.
@@ -657,10 +657,9 @@ Proof.
 Qed.
 
 (** For compatibility, can be deduced from [InfA_compat] *)
-Lemma InfA_eqA :
- forall l x y, eqA x y -> InfA y l -> InfA x l.
-Proof.
- intros l x y H; rewrite H; auto.
+Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
+Proof using eqA_equiv ltA_compat.
+ intros H; now rewrite H.
 Qed.
 Hint Immediate InfA_ltA InfA_eqA.
 
-- 
cgit v1.2.3