Generalized binding syntax overhaul: only two new binders: `() and `{},

guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards 
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or 
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).


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

10 files changed, 107 insertions, 120 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index b530cc0989..91c417ce3d 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -15,8 +14,7 @@
 
 (* $Id$ *)
 
-Set Implicit Arguments.
-Unset Strict Implicit.
+Set Manual Implicit Arguments.
 
 (** Export notations. *)
 
@@ -29,12 +27,12 @@ Require Import Coq.Logic.Decidable.
 
 Open Scope equiv_scope.
 
-Class [ equiv : Equivalence A ] => DecidableEquivalence :=
+Class DecidableEquivalence `(equiv : Equivalence A) :=
   setoid_decidable : forall x y : A, decidable (x === y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ equiv : Equivalence A ] => EqDec :=
+Class EqDec A R {equiv : Equivalence R} :=
   equiv_dec : forall x y : A, { x === y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -54,7 +52,7 @@ Open Local Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
+Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -62,10 +60,10 @@ Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition equiv_decb `{EqDec A} (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb `{EqDec A} (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -77,15 +75,15 @@ Require Import Coq.Arith.Peano_dec.
 
 (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
-Program Instance nat_eq_eqdec : ! EqDec nat eq :=
+Program Instance nat_eq_eqdec : EqDec nat eq :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : ! EqDec bool eq :=
+Program Instance bool_eqdec : EqDec bool eq :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : ! EqDec unit eq :=
+Program Instance unit_eqdec : EqDec unit eq :=
   equiv_dec x y := in_left.
 
   Next Obligation.
@@ -94,7 +92,7 @@ Program Instance unit_eqdec : ! EqDec unit eq :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
+Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
   ! EqDec (prod A B) eq :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
@@ -106,8 +104,8 @@ Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
 
   Solve Obligations using unfold complement, equiv ; program_simpl.
 
-Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
-  ! EqDec (sum A B) eq :=
+Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
+  EqDec (sum A B) eq :=
   equiv_dec x y := 
     match x, y with
       | inl a, inl b => if a == b then in_left else in_right
@@ -121,7 +119,7 @@ Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
+Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
@@ -138,7 +136,7 @@ Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
 
 Require Import List.
 
-Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
+Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
   equiv_dec := 
     fix aux (x : list A) y { struct x } :=
     match x, y with
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 469147cf44..3fcbac0619 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -27,7 +27,7 @@ Unset Strict Implicit.
 
 Open Local Scope signature_scope.
 
-Definition equiv [ Equivalence A R ] : relation A := R.
+Definition equiv `{Equivalence A R} : relation A := R.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -39,7 +39,7 @@ Open Local Scope equiv_scope.
 
 (** Overloading for [PER]. *)
 
-Definition pequiv [ PER A R ] : relation A := R.
+Definition pequiv `{PER A R} : relation A := R.
 
 (** Overloaded notation for partial equivalence. *)
 
@@ -47,11 +47,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
 
-Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
 
-Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -103,10 +103,10 @@ Section Respecting.
   (** Here we build an equivalence instance for functions which relates respectful ones only, 
      we do not export it. *)
 
-  Definition respecting {( eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B) )} : Type := 
+  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] :
+  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
   
   Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
@@ -120,7 +120,7 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence A ((eqb : Equivalence B eqB)) :
+Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
   Equivalence (pointwise_relation A eqB) | 9.
 
   Next Obligation.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index c3a00259b1..602b7b09dd 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -21,22 +20,22 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : 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 Surjective `(m : Morphism (A -> B) (RA ++> RB) f) : 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 MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) :=
+Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
   monic :> Injective m.
 
-Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
+Class EpiMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
   epic :> Surjective m.
 
-Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
-  monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
+Class IsoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
+  { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }.
 
-Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ I : ! IsoMorphism m ] => AutoMorphism.
+Class AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 5e7504c55b..111d85f742 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -95,7 +95,7 @@ Hint Unfold Transitive : core.
 
 Typeclasses Opaque respectful pointwise_relation forall_relation.
 
-Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
+Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) : 
   PER (R ==> R').
 
   Next Obligation.
@@ -107,12 +107,12 @@ Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B
 
 (** Subrelations induce a morphism on the identity. *)
 
-Instance subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id.
 Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] :
+Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
   subrelation (R₁ ==> S₁) (R₂ ==> S₂).
 Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
@@ -123,8 +123,8 @@ Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
-  sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
+Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
+  sub : subrelation A R₁ R₂) : Morphism R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
@@ -157,14 +157,14 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance pointwise_subrelation A ((sub : subrelation B R R')) :
+Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
   subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
 Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
 Program Instance complement_morphism
-  [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] :
+  `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
   Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
@@ -177,7 +177,7 @@ Program Instance complement_morphism
 (** The [inverse] too, actually the [flip] instance is a bit more general. *) 
 
 Program Instance flip_morphism
-  [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] :
+  `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
   Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
@@ -189,7 +189,7 @@ Program Instance flip_morphism
    contravariant in the first argument, covariant in the second. *)
 
 Program Instance trans_contra_co_morphism
-  [ Transitive A R ] : Morphism (R --> R ++> impl) R.
+  `(Transitive A R) : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -200,7 +200,7 @@ Program Instance trans_contra_co_morphism
 (** Morphism declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3.
+  `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -208,7 +208,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3.
+  `(Transitive A R) : Morphism (R ==> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -216,7 +216,7 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2.
+  `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -224,7 +224,7 @@ Program Instance trans_sym_co_inv_impl_morphism
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  [ PER A R ] : Morphism (R --> impl) (R x) | 2.
+  `(PER A R) : Morphism (R --> impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -232,7 +232,7 @@ Program Instance trans_sym_contra_impl_morphism
   Qed.
 
 Program Instance per_partial_app_morphism
-  [ PER A R ] : Morphism (R ==> iff) (R x) | 1.
+  `(PER A R) : Morphism (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
@@ -246,7 +246,7 @@ Program Instance per_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
+  `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
@@ -255,7 +255,7 @@ Program Instance trans_co_eq_inv_impl_morphism
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
+Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -265,7 +265,7 @@ Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
     transitivity y... transitivity y0... symmetry...
   Qed.
 
-Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R).
+Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
 Proof. firstorder. Qed.
   
 Program Instance compose_morphism A B C R₀ R₁ R₂ :
@@ -280,7 +280,7 @@ Program Instance compose_morphism A B C R₀ R₁ R₂ :
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
+Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -315,16 +315,16 @@ Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
 Instance reflexive_morphism_proxy
-  [ Reflexive A R ] (x : A) : MorphismProxy R x | 1.
+  `(Reflexive A R) (x : A) : MorphismProxy R x | 1.
 Proof. firstorder. Qed.
 
 Instance morphism_morphism_proxy
-  [ Morphism A R x ] : MorphismProxy R x | 2.
+  `(Morphism A R x) : MorphismProxy R x | 2.
 Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
+Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
    Morphism R' (m x).
 Proof. simpl_relation. Qed.
 
@@ -403,7 +403,7 @@ Qed.
 
 (** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
 
-Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
+Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := 
   normalizes : relation_equivalence m m'.
 
 (** Current strategy: add [inverse] everywhere and reduce using [subrelation]
@@ -414,7 +414,7 @@ Proof.
   firstorder.
 Qed.
 
-Lemma inverse_arrow ((NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R''))) :
+Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
   Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
 Proof. unfold Normalizes. intros.
   rewrite NA, NB. firstorder.
@@ -431,10 +431,10 @@ Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
 (** Treating inverse: can't make them direct instances as we 
    need at least a [flip] present in the goal. *)
 
-Lemma inverse1 ((subrelation A R' R)) : subrelation (inverse (inverse R')) R.
+Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
 Proof. firstorder. Qed.
 
-Lemma inverse2 ((subrelation A R R')) : subrelation R (inverse (inverse R')).
+Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
 Proof. firstorder. Qed.
 
 Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
@@ -442,7 +442,7 @@ Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor.
+Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.
 
 Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.
 
@@ -459,7 +459,7 @@ Proof.
   apply H0.
 Qed.
 
-Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
+Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.
 Proof.
   intros.
 
@@ -481,7 +481,7 @@ Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
 
 (** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
 
-Lemma reflexive_morphism [ Reflexive A R ] (x : A)
+Lemma reflexive_morphism `{Reflexive A R} (x : A)
    : Morphism R x.
 Proof. firstorder. Qed.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index d286b190f7..b9256bdbc0 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -71,31 +70,31 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
-Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) :=
+Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) :=
+Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R).
+Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
 
-Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R).
+Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
 
-Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R).
+Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
 
-Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ]
+Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
    : Irreflexive (complement R).
 
   Next Obligation. 
   Proof. firstorder. Qed.
 
-Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
+Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
 
   Next Obligation.
   Proof. firstorder. Qed.
@@ -149,35 +148,35 @@ Program Instance eq_Transitive : Transitive (@eq A).
 
 (** A [PreOrder] is both Reflexive and Transitive. *)
 
-Class PreOrder {A} (R : relation A) : Prop :=
+Class PreOrder {A} (R : relation A) : Prop := {
   PreOrder_Reflexive :> Reflexive R ;
-  PreOrder_Transitive :> Transitive R.
+  PreOrder_Transitive :> Transitive R }.
 
 (** A partial equivalence relation is Symmetric and Transitive. *)
 
-Class PER {A} (R : relation A) : Prop :=
+Class PER {A} (R : relation A) : Prop := {
   PER_Symmetric :> Symmetric R ;
-  PER_Transitive :> Transitive R.
+  PER_Transitive :> Transitive R }.
 
 (** Equivalence relations. *)
 
-Class Equivalence {A} (R : relation A) : Prop :=
+Class Equivalence {A} (R : relation A) : Prop := {
   Equivalence_Reflexive :> Reflexive R ;
   Equivalence_Symmetric :> Symmetric R ;
-  Equivalence_Transitive :> Transitive R.
+  Equivalence_Transitive :> Transitive R }.
 
 (** An Equivalence is a PER plus reflexivity. *)
 
-Instance Equivalence_PER [ Equivalence A R ] : PER R | 10 :=
+Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
   PER_Symmetric := Equivalence_Symmetric ;
   PER_Transitive := Equivalence_Transitive.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := 
+Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} :
+Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
   ! Antisymmetric A eqA (flip R).
 
 (** Leibinz equality [eq] is an equivalence relation.
@@ -369,14 +368,14 @@ 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 ((equ : Equivalence A eqA)) ((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 
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
-Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA 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. 
   apply <- poe. firstorder.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 17bd4a6d72..9441738937 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -22,10 +21,10 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-(* Application of the extensionality axiom to turn a goal on leibinz equality to 
-   a setoid equivalence. *)
+(* Application of the extensionality axiom to turn a goal on 
+   Leibinz equality to a setoid equivalence (use with care!). *)
 
-Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
 
 (** Application of the extensionality principle for setoids. *)
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index ddefa5cd7a..78616a9a42 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -26,9 +26,9 @@ Require Import Coq.Classes.Functions.
 
 (** A setoid wraps an equivalence. *)
 
-Class Setoid A :=
+Class Setoid A := {
   equiv : relation A ;
-  setoid_equiv :> Equivalence equiv.
+  setoid_equiv :> Equivalence equiv }.
 
 (* Too dangerous instance *)
 (* Program Instance [ eqa : Equivalence A eqA ] =>  *)
@@ -37,13 +37,13 @@ Class Setoid A :=
 
 (** Shortcuts to make proof search easier. *)
 
-Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Definition setoid_refl `(sa : Setoid A) : Reflexive equiv.
 Proof. typeclasses eauto. Qed.
 
-Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Definition setoid_sym `(sa : Setoid A) : Symmetric equiv.
 Proof. typeclasses eauto. Qed.
 
-Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Definition setoid_trans `(sa : Setoid A) : Transitive equiv.
 Proof. typeclasses eauto. Qed.
 
 Existing Instance setoid_refl.
@@ -55,7 +55,7 @@ Existing Instance setoid_trans.
 (* Program Instance eq_setoid : Setoid A := *)
 (*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
-Program Instance iff_setoid : Setoid Prop :=
+Program Instance iff_setoid : Setoid Prop := 
   equiv := iff ; setoid_equiv := iff_equivalence.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -84,7 +84,7 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof with auto.
   intros; intro.
   assert(z == y) by (symmetry ; auto).
@@ -92,7 +92,7 @@ Proof with auto.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y == x) by (symmetry ; auto).
@@ -119,18 +119,11 @@ Ltac setoidify := repeat setoidify_tac.
 
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
-Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
-  PER_morphism.
+Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv :=
+  respect := respect.
 
-(** Add this very useful instance in the database. *)
-
-Implicit Arguments setoid_morphism [[!sa]].
-Existing Instance setoid_morphism.
-
-Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism.
-
-Existing Instance setoid_partial_app_morphism.
+Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) :=
+  respect := respect.
 
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
@@ -144,9 +137,8 @@ Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id.
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-Class PartialSetoid (A : Type) :=
-  pequiv : relation A ;
-  pequiv_prf :> PER pequiv.
+Class PartialSetoid (A : Type) := 
+  { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
 (** Overloaded notation for partial setoid equivalence. *)
 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index ab1fc1ca69..5b44f68481 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -26,12 +26,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class DecidableSetoid [ S : Setoid A ] :=
+Class DecidableSetoid `(S : Setoid A) :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class (( S : Setoid A )) => EqDec :=
+Class EqDec `(S : Setoid A) :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -51,7 +51,7 @@ Open Local Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -59,10 +59,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition equiv_decb `{EqDec A} (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb `{EqDec A} (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -94,7 +94,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 
@@ -109,7 +109,7 @@ Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : E
 
 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 024b400ae0..70c8d69077 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -45,11 +45,11 @@ Class DefaultRelation A (R : relation A).
 
 (** To search for the default relation, just call [default_relation]. *)
 
-Definition default_relation [ DefaultRelation A R ] := R.
+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 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. *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 6a5eafe8bf..1e19f66b81 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -276,14 +276,14 @@ Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discrimi
    [injection] tactics on which we can always fall back.
    *)
   
-Class NoConfusionPackage (I : Type) := NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P.
+Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
 
 (** The [DependentEliminationPackage] provides the default dependent elimination principle to
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
 Class DependentEliminationPackage (A : Type) :=
-  elim_type : Type ; elim : elim_type.
+  { elim_type : Type ; elim : elim_type }.
 
 (** A higher-order tactic to apply a registered eliminator. *)
 
@@ -302,14 +302,14 @@ Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
 (** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
    allowing to talk about course-of-value recursion on it. *)
 
-Class BelowPackage (A : Type) :=
+Class BelowPackage (A : Type) := {
   Below : A -> Type ;
-  below : Π (a : A), Below a.
+  below : Π (a : A), Below a }.
 
 (** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
 
 Class Recursor (A : Type) (BP : BelowPackage A) := 
-  rec_type : A -> Type ; rec : Π (a : A), rec_type a.
+  { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
 
 (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)