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

22 files changed, 184 insertions, 213 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 62f1148320..67ae85d648 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1370,7 +1370,7 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
@@ -1385,7 +1385,7 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index f41d88bd60..d6ef1ea3b6 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -107,9 +107,9 @@ let convert_one_inductive sp tyi =
   let env = Global.env () in
   let envpar = push_rel_context params env in
   let sp = sp_of_global (IndRef (sp, tyi)) in
-  (((dummy_loc,basename sp),
+  (((false,(dummy_loc,basename sp)),
    convert_env(List.rev params),
-   Some (extern_constr true envpar arity),
+   Some (extern_constr true envpar arity), None,
    Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
 
 (* This function converts a Mutual inductive definition to a Coqast.t.
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b404478ffb..6d6a0c0656 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1969,22 +1969,22 @@ let rec xlate_vernac =
 	       translated_restriction)
   	| SearchAbout [] -> assert false)
 
-  | (*Record from tactics/Record.v *)
-    VernacRecord 
-      (_, (add_coercion, (_,s)), binders, c1,
-       rec_constructor_or_none, field_list) ->
-      let record_constructor =
-        xlate_ident_opt (Option.map snd rec_constructor_or_none) in
-      CT_record
-       ((if add_coercion then CT_coercion_atm else
-          CT_coerce_NONE_to_COERCION_OPT(CT_none)),
-        xlate_ident s, xlate_binder_list binders, 
-	xlate_formula (Option.get c1), record_constructor,
-         build_record_field_list field_list)
+(*   | (\*Record from tactics/Record.v *\) *)
+(*     VernacRecord  *)
+(*       (_, (add_coercion, (_,s)), binders, c1, *)
+(*        rec_constructor_or_none, field_list) -> *)
+(*       let record_constructor = *)
+(*         xlate_ident_opt (Option.map snd rec_constructor_or_none) in *)
+(*       CT_record *)
+(*        ((if add_coercion then CT_coercion_atm else *)
+(*           CT_coerce_NONE_to_COERCION_OPT(CT_none)), *)
+(*         xlate_ident s, xlate_binder_list binders,  *)
+(* 	xlate_formula (Option.get c1), record_constructor, *)
+(*          build_record_field_list field_list) *)
    | VernacInductive (isind, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
       let strip_mutind = function
-          (((_,s), parameters, c, Constructors constructors), notopt) ->
+          (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->
           CT_ind_spec
             (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c),
              build_constructors constructors,
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index a240744bfc..510229ae6f 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -137,7 +137,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let sigma = Evd.evars_of !isevars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let subst = 
-    let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in
+    let props = match props with CRecord (loc, _, fs) -> fs
+      | _ -> errorlabstrm "new_instance" (Pp.str "Expected a record declaration for the instance body") 
+    in
       if List.length props > List.length k.cl_props then 
 	Classes.mismatched_props env' (List.map snd props) k.cl_props;
       match k.cl_props with 
diff --git a/ide/coq.ml b/ide/coq.ml
index 2f496d99d8..809c502e7e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -230,7 +230,6 @@ let rec attribute_of_vernac_command = function
   (* Gallina extensions *)
   | VernacBeginSection _ -> []
   | VernacEndSegment _ -> []
-  | VernacRecord _ -> []
   | VernacRequire _ -> []
   | VernacImport _ -> []
   | VernacCanonical _ -> []
@@ -386,7 +385,7 @@ let compute_reset_info = function
 
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
+  | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) ->
       ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
 
   | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6587b71367..a8dad2216a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -716,7 +716,7 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
 	    let id = 
 	      match ty with
 	      | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
-	      | _ -> id_of_string "assum"
+	      | _ -> id_of_string "H"
 	    in Implicit_quantifiers.make_fresh ids (Global.env ()) id
 	  in Name name
     | _ -> na
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e3b61e1b1..37c09704e6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -241,8 +241,8 @@ GEXTEND Gram
   ;
   record_declaration:
     [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
-      | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" ->
-	  CRecord (loc, Some c, fs)
+(*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
+(* 	  CRecord (loc, Some c, fs) *)
     ] ]
   ;
   record_field_declaration:
@@ -432,15 +432,9 @@ GEXTEND Gram
         [LocalRawAssum ([id],Default Implicit,c)]
     | "{"; id=name; idl=LIST1 name; "}" -> 
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
-    | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc
-    | "{"; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; "}" ->
+    | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
-    | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
-    | "("; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Implicit, b), t)) tc
-    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+    | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d870c85eb0..4ffd53fe4e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -170,10 +170,11 @@ GEXTEND Gram
     [ [ b = record_token; oc = opt_coercion; name = identref;
         ps = binders_let; 
 	s = OPT [ ":"; s = lconstr -> s ];
-	":="; cstr = OPT identref; "{";
-        fs = LIST0 record_field SEP ";"; "}" ->
-	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
-    ] ]
+	cfs = [ ":="; l = constructor_list_or_record_decl -> l
+	  | -> RecordDecl (None, []) ] ->
+	  let (recf,indf) = b in
+	    VernacInductive (indf,[((oc,name),ps,s,Some recf,cfs),None])
+  ] ]
   ;
   typeclass_context:
     [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l 
@@ -222,7 +223,7 @@ GEXTEND Gram
   record_token:
     [ [ IDENT "Record" -> (Record,true)
       | IDENT "Structure" -> (Structure,true) 
-      | IDENT "Class" -> (Class,true) ] ]
+      | IDENT "Class" -> (Class true,true) ] ]
   ;
   (* Simple definitions *)
   def_body:
@@ -245,19 +246,19 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = binders_let; 
+    [ [ id = identref; oc = opt_coercion; indpar = binders_let; 
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
-	   ((id,indpar,c,lc),ntn) ] ]
+	   (((oc,id),indpar,c,None,lc),ntn) ] ]
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
       | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> 
-	      Constructors ((c id)::l)
+	  Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
       | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
-	     RecordDecl (Record,Some cstr,fs) 
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (Record,None,fs) 
+	  RecordDecl (Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) 
       |  -> Constructors [] ] ]
   ;
 (*
@@ -500,20 +501,6 @@ GEXTEND Gram
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
-
-      (* Type classes, new syntax without artificial sup. *)
-      | IDENT "Class"; qid = identref; pars = binders_let;
-           s = OPT [ ":"; c = lconstr -> c ];
-	   fs = class_fields ->
-	   VernacInductive (false, [((qid,pars,s,RecordDecl (Class,None,fs)),None)])
-
-      (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
-	 qid = identref; pars = binders_let;
-         s = OPT [ ":"; c = lconstr -> c ];
-	 fs = class_fields ->
-	   VernacInductive 
-	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (Class,None,fs)),None)])
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
@@ -547,10 +534,6 @@ GEXTEND Gram
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
-  class_fields:
-    [ [ ":="; fs = LIST1 record_field SEP ";" -> fs
-      | -> [] ] ]
-  ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
     | id = ident -> (id,false,false)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 01e44f84c9..33c7654d25 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -582,24 +582,31 @@ let rec pr_vernac = function
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
                 pr_spc_lconstr c) in
-      let pr_constructor_list l = match l with
+      let pr_constructor_list b l = match l with
         | Constructors [] -> mt()
         | Constructors l ->
             pr_com_at (begin_of_inductive l) ++
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l 
-       | RecordDecl (b,c,fs) ->   
+       | RecordDecl (c,fs) ->   
 	    spc() ++
 	    pr_record_decl b c fs in
-      let pr_oneind key ((id,indpar,s,lc),ntn) =
-	hov 0 (
-          str key ++ spc() ++
-          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ 
-	    Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
-	  str" :=") ++ pr_constructor_list lc ++ 
-	pr_decl_notation pr_constr ntn in
-
+      let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+	let kw =
+	  match k with
+	  | None -> str key
+	  | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" 
+	    | Class b -> if b then "Definitional Class" else "Class")
+	in
+	  hov 0 (
+	    kw ++ spc() ++
+              (if coe then str" > " else str" ") ++ pr_lident id ++
+              pr_and_type_binders_arg indpar ++ spc() ++ 
+	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
+	      str" :=") ++ pr_constructor_list k lc ++ 
+	    pr_decl_notation pr_constr ntn 
+      in
       hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
       ++ 
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
@@ -665,12 +672,6 @@ let rec pr_vernac = function
 	
 
   (* Gallina extensions *)
-  | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
-      hov 2
-        (str (match b with Record -> "Record" | Structure -> "Structure" | Class -> "Class") ++
-         (if oc then str" > " else str" ") ++ pr_lident name ++ 
-          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
-	  Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b c fs)
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2
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]. *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 59559f9234..79d34e878e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -274,7 +274,7 @@ let declare_instance_cst glob con =
       | Some tc -> add_instance (new_instance tc None glob con)
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
-let declare_class finite id idbuild paramimpls params arity fieldimpls fields
+let declare_class finite def id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers =
   let fieldimpls = 
     (* Make the class and all params implicits in the projections *)
@@ -284,7 +284,7 @@ let declare_class finite id idbuild paramimpls params arity fieldimpls fields
   in
   let impl, projs =
     match fields with
-    | [(Name proj_name, _, field)] ->
+    | [(Name proj_name, _, field)] when def ->
 	let class_body = it_mkLambda_or_LetIn field params in
 	let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
 	let class_entry =
@@ -373,5 +373,5 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
 	in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
-    | Class ->
-	declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+    | Class b ->
+	declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5f5dab6146..f5603535b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -387,7 +387,7 @@ let vernac_record k finite struc binders sort nameopt cfs =
       
 let vernac_inductive finite indl = 
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, cstrs), _) ->
+    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with 
 	| Constructors cstrs ->
 	    Dumpglob.dump_definition lid false "ind";
@@ -396,12 +396,22 @@ let vernac_inductive finite indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( id , bl , c ,RecordDecl (b,oc,fs) ), None ] -> 
-      vernac_record b finite (false,id) bl c oc fs
-  | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> 
+  | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> 
+      vernac_record (match b with Class true -> Class false | _ -> b)
+	finite id bl c oc fs
+  | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> 
+      let f = 
+	let (coe, ((loc, id), ce)) = l in
+	  ((coe, AssumExpr ((loc, Name id), ce)), None)
+      in vernac_record (Class true) finite id bl c None [f]
+  | [ ( id , bl , c , Some (Class true), _), _ ] -> 
+      Util.error "Definitional classes must have a single method"
+  | [ ( id , bl , c , Some (Class false), Constructors _), _ ] ->
+      Util.error "Inductive classes not supported"
+  | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> 
       Util.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function 
-      | ( id , bl , c , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
+      | ( (_, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
       | _ -> Util.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
@@ -1314,7 +1324,6 @@ let interp c = match c with
 
   | VernacEndSegment lid -> vernac_end_segment lid
 
-  | VernacRecord ((k,finite),id,bl,s,idopt,fs) -> vernac_record k finite id bl s idopt fs
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
@@ -1322,8 +1331,6 @@ let interp c = match c with
   | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
   (* Type classes *)
-(*   | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props *)
-
   | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance id -> vernac_declare_instance id
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5fff24fef7..8e797a8834 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -155,7 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type record_kind = Record | Structure | Class
+type record_kind = Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
@@ -164,9 +164,10 @@ type 'a with_notation = 'a * decl_notation
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of record_kind * lident option * local_decl_expr with_coercion with_notation list
+  | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-  lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr
+  lident with_coercion * local_binder list * constr_expr option * record_kind option * 
+    constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast
 
@@ -217,9 +218,6 @@ type vernac_expr =
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
-  | VernacRecord of (record_kind*bool) (* = Structure or Class * Inductive or CoInductive *)
-      * lident with_coercion * local_binder list
-      * constr_expr option * lident option * local_decl_expr with_coercion with_notation list
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of