From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 theories/Setoids/Setoid.v | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'theories/Setoids/Setoid.v')

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index a187a7c6..db4d699f 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*)
+(*i $Id$: i*)
 
 Require Export Coq.Classes.SetoidTactics.
 
-Export Morphisms.MorphismNotations.
+Export Morphisms.ProperNotations.
 
 (** For backward compatibility *)
 
@@ -18,46 +18,46 @@ Definition Setoid_Theory := @Equivalence.
 Definition Build_Setoid_Theory := @Build_Equivalence.
 
 Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
-  unfold Setoid_Theory. intros ; reflexivity.
+  unfold Setoid_Theory in s. intros ; reflexivity.
 Defined.
 
 Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x.
-  unfold Setoid_Theory. intros ; symmetry ; assumption.
+  unfold Setoid_Theory in s. intros ; symmetry ; assumption.
 Defined.
 
 Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z.
-  unfold Setoid_Theory. intros ; transitivity y ; assumption.
+  unfold Setoid_Theory in s. intros ; transitivity y ; assumption.
 Defined.
 
-(** Some tactics for manipulating Setoid Theory not officially 
+(** Some tactics for manipulating Setoid Theory not officially
     declared as Setoid. *)
 
 Ltac trans_st x :=
   idtac "trans_st on Setoid_Theory is OBSOLETE";
   idtac "use transitivity on Equivalence instead";
   match goal with
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_trans _ _ H) with x; auto
   end.
 
 Ltac sym_st :=
   idtac "sym_st on Setoid_Theory is OBSOLETE";
   idtac "use symmetry on Equivalence instead";
-  match goal with 
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+  match goal with
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_sym _ _ H); auto
   end.
 
 Ltac refl_st :=
   idtac "refl_st on Setoid_Theory is OBSOLETE";
   idtac "use reflexivity on Equivalence instead";
-  match goal with 
-    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+  match goal with
+    | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
       apply (Seq_refl _ _ H); auto
   end.
 
 Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
-Proof. 
-  constructor; congruence. 
+Proof.
+  constructor; congruence.
 Qed.
-  
+
-- 
cgit v1.2.3