From 835f581b40183986e76e5e02a26fab05239609c9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 26 Dec 2008 22:26:30 +0000
Subject: FMaps: various updates (mostly suggested by P. Casteran)

- New functions: update (a kind of union), restrict (a kind of inter),
   diff.
- New predicat Partition (and Disjoint), many results about Partition.
- Equivalence instead of obsolete Setoid_Theory (they are aliases).
  refl_st, sym_st, trans_st aren't used anymore and marked as obsolete.
- Start using Morphism (E.eq==>...) instead of compat_...
  This change (FMaps only) is incompatible with 8.2betaX, but it's really
  better now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Setoids/Setoid.v | 37 +++++++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 14 deletions(-)

(limited to 'theories/Setoids')

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 28d8feeae..613cabbd0 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -30,20 +30,29 @@ Defined.
 (** Some tactics for manipulating Setoid Theory not officially 
     declared as Setoid. *)
 
-Ltac trans_st x := match goal with 
-		     | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-		       apply (Seq_trans _ _ H) with x; auto
-		   end.
-
-Ltac sym_st := match goal with 
-		 | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-		   apply (Seq_sym _ _ H); auto
-	       end.
-
-Ltac refl_st := match goal with 
-		  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-		    apply (Seq_refl _ _ H); auto
-		end.
+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 _ _ => 
+      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 _ _ => 
+      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 _ _ => 
+      apply (Seq_refl _ _ H); auto
+  end.
 
 Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
 Proof. 
-- 
cgit v1.2.3