From 5dc1e83de7d933dccd9b8590b77e1c3d4cec593c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 30 Oct 2007 15:02:26 +0000
Subject: A useless Add Morphism: since Subset is a Setoid Relation, it is also
 automatically a Morphism about itself (avoid a warning about redeclared
 Setoids).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10277 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetFacts.v     | 5 -----
 theories/FSets/FSetWeakFacts.v | 5 -----
 2 files changed, 10 deletions(-)

diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 7eb9b04f63..4de3480d05 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -469,11 +469,6 @@ unfold Subset; intros s s' H s'' s''' H0 a.
 do 2 rewrite diff_iff; intuition.
 Qed.
 
-Add Morphism Subset with signature Subset --> Subset ++> impl as  Subset_s_m.
-Proof.
-unfold Subset, impl; auto.
-Qed.
-
 (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
    without additional hypothesis on [f]. For instance: *)
 
diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
index ff98648dc5..12bef504d9 100644
--- a/theories/FSets/FSetWeakFacts.v
+++ b/theories/FSets/FSetWeakFacts.v
@@ -466,11 +466,6 @@ unfold Subset; intros s s' H s'' s''' H0 a.
 do 2 rewrite diff_iff; intuition.
 Qed.
 
-Add Morphism Subset with signature Subset --> Subset ++> impl as  Subset_s_m.
-Proof.
-unfold Subset, impl; auto.
-Qed.
-
 (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
    without additional hypothesis on [f]. For instance: *)
 
-- 
cgit v1.2.3