diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-22 12:09:18 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-22 12:09:18 +0000 |
| commit | d08282cb2242d642d8ea40e844dbe61b7404674c (patch) | |
| tree | d1a8aa04194ed5c9adae5ec923915e12c8de5b28 /theories/Lists/SetoidList.v | |
| parent | 7511435a39d70625cde2949ddcc70684525a87e9 (diff) | |
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
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 6c573a127..f6eab8649 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. |