9 files changed, 47 insertions, 67 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 157217ae..15cabf81 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,9 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Export notations. *)
 
@@ -144,9 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
 
-  Next Obligation.
-  Proof. clear aux. red in H0. subst. 
-    destruct y; intuition (discriminate || eauto).
-  Defined.
+  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5e5895ab..7068bc6b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,15 +12,15 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *) 
 
-(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 5df7a4ed..762cc5c1 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,12 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
-
-Tactic Notation "clapply" ident(c) :=
-  eapply @c ; typeclasses eauto.
+(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
@@ -29,12 +24,12 @@ Typeclasses Opaque id const flip compose arrow impl iff.
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
-Class Unconvertible (A : Type) (a b : A).
+Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
 
 Ltac unconvertible :=
   match goal with
     | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
-    | |- _ => eapply Build_Unconvertible 
+    | |- _ => exact tt
   end.
 
 Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
 \ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 86097a56..2b653e27 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,9 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -55,18 +52,24 @@ Definition respectful {A B : Type}
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+
 Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
-  (right associativity, at level 55) : signature_scope.
+Module MorphismNotations.
 
-Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
 
-Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+End MorphismNotations.
 
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Export MorphismNotations.
 
 Open Local Scope signature_scope.
 
@@ -118,7 +121,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Instance morphisms_subrelation_refl : ! subrelation A R R.
 Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -151,10 +154,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Instance iff_impl_subrelation : subrelation iff impl.
+Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
 Proof. firstorder. Qed.
 
 Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
@@ -372,25 +375,6 @@ Ltac partial_application_tactic :=
       end
   end.
 
-Section PartialAppTest.
-  Instance and_ar : Params and 0.
-
-  Goal Morphism (iff) (and True True).
-    partial_application_tactic.
-  Admitted.
-
-  Goal Morphism (iff) (or True True).
-    partial_application_tactic.
-    partial_application_tactic. 
-  Admitted.
-
-  Goal Morphism (iff ==> iff) (iff True).
-    partial_application_tactic.
-    (*partial_application_tactic. *)
-   Admitted.
-
-End PartialAppTest.
-
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 24b8d636..4654e654 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -12,6 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
    91405 Orsay, France *)
 
+Require Import Relation_Definitions.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Program.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f95894be..e1de9ee9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -13,12 +13,12 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 
 (** We allow to unfold the [relation] definition while doing morphism search. *)
 
@@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
@@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal. 
+  pose proof partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
 Qed.
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 305168ec..03bb9a80 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃƒcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
 
 Require Import Coq.Program.Program.
 
@@ -22,7 +22,7 @@ Unset Strict Implicit.
 Require Export Coq.Classes.SetoidClass.
 
 (* Application of the extensionality axiom to turn a goal on 
-   Leibinz equality to a setoid equivalence (use with care!). *)
+   Leibniz equality to a setoid equivalence (use with care!). *)
 
 Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 47f92ada..d3da7d5a 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,14 +12,14 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Import Coq.Program.Program.
 
-Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Import Coq.Classes.Functions.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index caacc9ec..36f05e31 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,13 +13,13 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+
+Export MorphismNotations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.