Fixes in handling of implicit arguments:

- Now [ id : Class foo ] makes id an explicit argument, 
  and [ Class foo ] is equivalent to [ {someid} : Class foo ].
  This makes declarations such as "Class Ord [ eq : Eq a ]" have
  sensible implicit args.
- Better handling of {} in class and record declarations, refactorize 
  code for declaring structures and classes.  
- Fix merging of implicit arguments information on section closing.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 16 insertions, 22 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3ffa8040d..2c1a7deb9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -321,11 +321,11 @@ Class MorphismProxy A (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
 Instance reflexive_morphism_proxy
-  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
+  [ Reflexive A R ] (x : A) : MorphismProxy R x | 1.
 Proof. firstorder. Qed.
 
 Instance morphism_morphism_proxy
-  [ Morphism A R x ] : MorphismProxy A R x | 2.
+  [ Morphism A R x ] : MorphismProxy R x | 2.
 Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -376,17 +376,17 @@ Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
 Instance inverse_respectful_norm : 
-  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
+  ! Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof. firstorder. Qed.
 
 (* If not an inverse on the left, do a double inverse. *)
 
 Instance not_inverse_respectful_norm : 
-  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+  ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
 Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
-  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+  ! Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
 Proof. red ; intros. 
   assert(r:=normalizes).
   setoid_rewrite r.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index c4e98c24a..99eda0ae1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -43,7 +43,7 @@ Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
 Class Irreflexive A (R : relation A) := 
-  irreflexivity :> Reflexive A (complement R).
+  irreflexivity :> Reflexive (complement R).
 
 Class Symmetric A (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
@@ -54,12 +54,6 @@ Class Asymmetric A (R : relation A) :=
 Class Transitive A (R : relation A) := 
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments Reflexive [A].
-Implicit Arguments Irreflexive [A].
-Implicit Arguments Symmetric [A].
-Implicit Arguments Asymmetric [A].
-Implicit Arguments Transitive [A].
-
 Hint Resolve @irreflexivity : ord.
 
 Unset Implicit Arguments.
@@ -178,7 +172,7 @@ Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
+Class [ equ : Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
 Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 4d6601a6e..07a6985c9 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class [ Setoid A ] => DecidableSetoid :=
+Class DecidableSetoid A [ Setoid A ] :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ Setoid A ] => EqDec :=
+Class [ s : Setoid A ] => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith.
 
 (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
-Program Instance eq_setoid : Setoid A :=
+Program Instance eq_setoid A : Setoid A :=
   equiv := eq ; setoid_equiv := eq_equivalence.
 
-Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
+Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
+Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
+Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
   equiv_dec x y := in_left.
 
   Next Obligation.
@@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
+Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -110,7 +110,7 @@ Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] :
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index ff5f7cb6c..e939d3ee7 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -38,7 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)