- Improve [Context] vernacular to allow arbitrary binders, not just

classes, and simplify the implementation.
- Experimental syntax {{ cl : Class args }} and (( cl : Class args ))
which respectively make cl an implicit or explicit argument ({{ }} is
equivalent to [ ]). Could be extended to any type of binder, eg. 
[Definition flip ((R : relation carrier)) : relation carrier := ...].
The idea behind double brackets is to distinguish macro-binders which 
perform implicit generalization from regular binders. It could also save
[ ] for other uses.
- Fix bug #1901 about {} binders in records.


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

3 files changed, 11 insertions, 11 deletions

diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 64eee17d8e..8da1c31762 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
-Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) :=
   Injective m /\ Surjective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) :=
   monic :> Injective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
   epic :> Surjective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
   monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
 
-Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
+Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 99eda0ae1b..ddd7b38da4 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -172,11 +172,11 @@ 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 [ equ : Equivalence A eqA ] => Antisymmetric (R : relation A) := 
+Class Antisymmetric ((equ : Equivalence A eqA)) (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 ] :
-  Antisymmetric eq (flip R).
+Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} :
+  ! Antisymmetric A eqA (flip R).
 
 (** Leibinz equality [eq] is an equivalence relation.
    The instance has low priority as it is always applicable 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 07a6985c97..8d40c19a5e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -32,7 +32,7 @@ Class DecidableSetoid A [ Setoid A ] :=
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ s : 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