More factorization of inductive/record and typeclasses: move class

declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.


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

25 files changed, 321 insertions, 402 deletions

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index b7cee7390..9bbd165df 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     List.map (* zeta_normalize t ? *)
       (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
       rawlist in  
-  lident , bindlist , cstr_expr , lcstor_expr
+  lident , bindlist , Some cstr_expr , lcstor_expr
 
 
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index c16e645c7..75f6207fc 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1192,7 +1192,7 @@ let do_build_inductive
   let rel_ind i ext_rel_constructors = 
     ((dummy_loc,relnames.(i)),
     rel_params,
-    rel_arities.(i),
+    Some rel_arities.(i),
     ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 7ee38fc23..f41d88bd6 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -109,7 +109,7 @@ let convert_one_inductive sp tyi =
   let sp = sp_of_global (IndRef (sp, tyi)) in
   (((dummy_loc,basename sp),
    convert_env(List.rev params),
-   (extern_constr true envpar arity),
+   Some (extern_constr true envpar arity),
    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 73acbf0f3..8ec6cfb2f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1979,14 +1979,14 @@ let rec xlate_vernac =
        ((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 c1, record_constructor,
+	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) ->
           CT_ind_spec
-            (xlate_ident s, xlate_binder_list parameters, xlate_formula c,
+            (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c),
              build_constructors constructors,
 	     translate_opt_notation_decl notopt)
         | _ -> xlate_error "TODO: Record notation in (Co)Inductive" in
@@ -2148,7 +2148,7 @@ let rec xlate_vernac =
 
     (* Type Classes *) 
    | VernacDeclareInstance _|VernacContext _|
-	 VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
+	 VernacInstance (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 7b8d982d1..150abd8d6 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -122,58 +122,61 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
   let id = 
     match snd instid with
-	Name id -> 
-	  let sp = Lib.make_path id in
-	    if Nametab.exists_cci sp then
-	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
-	    id
-      | Anonymous -> 
-	  let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
-	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
+    | Name id -> 
+	let sp = Lib.make_path id in
+	  if Nametab.exists_cci sp then
+	    errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+	  id
+    | Anonymous -> 
+	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
+	  Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
   let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = List.map (Evarutil.nf_evar sigma) subst in
-  let subst, _propsctx = 
-    let props = 
-      List.map (fun (x, l, d) -> 
-	x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
-	props
-    in
+  let subst = 
+    let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in
       if List.length props > List.length k.cl_props then 
 	Classes.mismatched_props env' (List.map snd props) k.cl_props;
-      let props, rest = 
-	List.fold_left
-	  (fun (props, rest) (id,_,_) -> 
-	    try 
-	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
-		c :: props, rest'
-	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
-	  ([], props) k.cl_props
-      in
-	if rest <> [] then 
-	  unbound_method env' k.cl_impl (fst (List.hd rest))
-	else
-	  type_ctx_instance isevars env' k.cl_props props substctx
+      match k.cl_props with 
+      | [(na,b,ty)] -> 
+	  let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
+	  let ty' = substl subst ty in
+	  let c = interp_casted_constr_evars isevars env' term ty' in
+	    c :: subst
+      | _ ->
+	  let props, rest = 
+	    List.fold_left
+	      (fun (props, rest) (id,_,_) -> 
+		try 
+		  let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+		  let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
+		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+		    c :: props, rest'
+		with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+	      ([], props) k.cl_props
+	  in
+	    if rest <> [] then 
+	      unbound_method env' k.cl_impl (fst (List.hd rest))
+	    else
+	      fst (type_ctx_instance isevars env' k.cl_props props substctx)
   in
   let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
-    isevars := Evarutil.nf_evar_defs !isevars;
-    let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
-    and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+  and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
+  in
+    isevars := undefined_evars !isevars;
+    Evarutil.check_evars env Evd.empty !isevars termtype;
+    let hook gr = 
+      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+      let inst = Typeclasses.new_instance k pri global cst in
+	Impargs.declare_manual_implicits false gr ~enriching:false imps;
+	Typeclasses.add_instance inst
     in
-      isevars := undefined_evars !isevars;
-      Evarutil.check_evars env Evd.empty !isevars termtype;
-      let hook gr = 
-	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-	let inst = Typeclasses.new_instance k pri global cst in
-	  Impargs.declare_manual_implicits false gr ~enriching:false imps;
-	  Typeclasses.add_instance inst
-      in
-      let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
-      let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
-	id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
-	  
+    let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+    let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+      id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
+	
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 583c1a165..917ed8059 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -34,9 +34,9 @@ val type_ctx_instance :     Evd.evar_defs ref ->
 
 val new_instance : 
   ?global:bool ->
-  Topconstr.local_binder list ->
+  local_binder list ->
   typeclass_constraint ->
-  binder_def_list ->
+  constr_expr ->
   ?generalize:bool ->
   int option ->
   identifier * Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 191400212..4876b0655 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -99,7 +99,7 @@ let interp_binder sigma env na t =
     SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
 
 let interp_context_evars evdref env params = 
-  let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+  let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
diff --git a/ide/coq.ml b/ide/coq.ml
index 2d8c2ff99..2f496d99d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -238,7 +238,6 @@ let rec attribute_of_vernac_command = function
   | VernacIdentityCoercion _ -> []
 
   (* Type classes *)
-  | VernacClass _ -> []
   | VernacInstance _ -> []
   | VernacContext _ -> []
   | VernacDeclareInstance _ -> []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 660da5525..6587b7136 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -680,44 +680,61 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
     pr_id id ++ strbrk " must not be used as a bound variable in the type \
 of its constructor.")
 
-let push_name_env lvar (ids,unb,tmpsc,scopes as env) = function
-  | Anonymous -> env 
+let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
+  | Anonymous -> 
+      if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
+      env
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
       (Idset.add id ids, unb,tmpsc,scopes)
 
-let push_loc_name_env lvar (ids,unb,tmpsc,scopes as env) loc = function
-  | Anonymous -> env 
+let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
+  | Anonymous -> 
+      if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
+      env
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
       Dumpglob.dump_binding loc id;
       (Idset.add id ids,unb,tmpsc,scopes)
 
-let intern_generalized_binder intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
+let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
+    (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
   let ty = 
     if t then ty else
       Implicit_quantifiers.implicit_application ids
 	Implicit_quantifiers.combine_params_freevar ty
   in
-  let ty = intern_type (ids,true,tmpsc,sc) ty in
-  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty in
-  let env' = List.fold_left (fun env (x, l) -> push_loc_name_env lvar env l (Name x)) env fvs in
+  let ty' = intern_type (ids,true,tmpsc,sc) ty in
+  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty' in
+  let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
   let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
-    (push_loc_name_env lvar env' loc na), (na,b',None,ty) :: List.rev bl
-      
-let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
+  let na = match na with
+    | Anonymous -> 
+	if fail_anonymous then na 
+	else
+	  let name = 
+	    let id = 
+	      match ty with
+	      | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
+	      | _ -> id_of_string "assum"
+	    in Implicit_quantifiers.make_fresh ids (Global.env ()) id
+	  in Name name
+    | _ -> na
+  in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
+
+let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
       | Default k ->
 	  let (loc,na) = List.hd nal in
-	    (* TODO: fail if several names with different implicit types *)
+	  (* TODO: fail if several names with different implicit types *)
 	  let ty = locate_if_isevar loc na (intern_type env ty) in
 	    List.fold_left
 	      (fun ((ids,unb,ts,sc),bl) (_,na) ->
 		((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
 	      (env,bl) nal
       | Generalized (b,b',t) ->
-	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
+	  let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in
 	    env, b @ bl)
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,unb,ts,sc),
@@ -1297,10 +1314,10 @@ let my_intern_constr sigma env lvar acc c =
 
 let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
-let intern_context sigma env params =
+let intern_context fail_anonymous sigma env params =
   let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
     snd (List.fold_left
-	    (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
+	    (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
 	    ((extract_ids env,false,None,[]), []) params)
 
 let interp_context_gen understand_type understand_judgment env bl = 
@@ -1322,17 +1339,17 @@ let interp_context_gen understand_type understand_judgment env bl =
 	  | Some b ->
 	      let c = understand_judgment env b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env,d::params, succ n, impls))
+		(push_rel d env, d::params, succ n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context sigma env params = 
-  let bl = intern_context sigma env params in
+let interp_context ?(fail_anonymous=false) sigma env params = 
+  let bl = intern_context fail_anonymous sigma env params in
     interp_context_gen (Default.understand_type sigma) 
       (Default.understand_judgment sigma) env bl
     
-let interp_context_evars evdref env params =
-  let bl = intern_context (Evd.evars_of !evdref) env params in
+let interp_context_evars ?(fail_anonymous=false) evdref env params =
+  let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in
     interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
       (Default.understand_judgment_tcc evdref) env bl
     
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1554d4289..a646b6314 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -67,7 +67,7 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
 
-val intern_context : evar_map -> env -> local_binder list -> raw_binder list
+val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
 
 (*s Composing internalisation with pretyping *)
 
@@ -126,9 +126,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
 
 (* Interpret contexts: returns extended env and context *)
 
-val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context : ?fail_anonymous:bool -> 
+  evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
-val interp_context_evars : 
+val interp_context_evars : ?fail_anonymous:bool -> 
   evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 (* Locating references of constructions, possibly via a syntactic definition *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b061da5a8..3e3b61e1b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -147,7 +147,7 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let
+  binder binder_let binders_let record_declaration
   binders_let_fixannot typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e1df1cf49..b48548f98 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -48,6 +48,7 @@ let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
 let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
+let record_field = Gram.Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
 
 let get_command_entry () =
@@ -129,7 +130,7 @@ let no_coercion loc (c,x) =
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_context typeclass_constraint decl_notation;
+    typeclass_context typeclass_constraint record_field decl_notation;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -168,7 +169,7 @@ GEXTEND Gram
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = identref;
         ps = binders_let; 
-	s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
+	s = OPT [ ":"; s = lconstr -> s ];
 	":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
@@ -243,7 +244,7 @@ GEXTEND Gram
   (* Inductives and records *)
   inductive_definition:
     [ [ id = identref; indpar = binders_let; 
-        c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
+        c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
 	   ((id,indpar,c,lc),ntn) ] ]
   ;
@@ -253,8 +254,8 @@ GEXTEND Gram
 	      Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
       | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
-	     RecordDecl (Some cstr,fs) 
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) 
+	     RecordDecl (false,Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (false,None,fs) 
       |  -> Constructors [] ] ]
   ;
 (*
@@ -500,16 +501,17 @@ GEXTEND Gram
 
       (* Type classes, new syntax without artificial sup. *)
       | IDENT "Class"; qid = identref; pars = binders_let;
-	 s = [ ":"; c = sort -> Some (loc, c) | -> None ];
-	 props = typeclass_field_types ->
-	   VernacClass (qid, pars, s, [], props)
+           s = OPT [ ":"; c = lconstr -> c ];
+	   fs = class_fields ->
+	   VernacInductive (false, [((qid,pars,s,RecordDecl (false,None,fs)),None)])
 
       (* Type classes *)
       | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
 	 qid = identref; pars = binders_let;
-	 s = [ ":"; c = sort -> Some (loc, c) | -> None ];
-	 props = typeclass_field_types ->
-	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
+         s = OPT [ ":"; c = lconstr -> c ];
+	 fs = class_fields ->
+	   VernacInductive 
+	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (false,None,fs)),None)])
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
@@ -517,7 +519,8 @@ GEXTEND Gram
       | IDENT "Instance"; local = non_locality; name = identref; 
 	 sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
+	 pri = OPT [ "|"; i = natural -> i ] ; 
+	 props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
 	   let sup =
 	     match sup with
 		 None -> []
@@ -542,26 +545,16 @@ 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)
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-  typeclass_field_type:
-    [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ]
-  ;
-  typeclass_field_def:
-    [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ]
-  ;
-  typeclass_field_types:
-    [ [ ":="; l = LIST1 typeclass_field_type SEP ";" -> l
-    | -> [] ] ]
-  ;
-  typeclass_field_defs:
-    [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l
-    | -> [] ] ]
-  ;
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 69c1164f1..ed4f41c4e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -445,6 +445,7 @@ module Constr =
     let binders_let = Gram.Entry.create "constr:binders_let"
     let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
+    let record_declaration = Gram.Entry.create "constr:record_declaration"
     let appl_arg = Gram.Entry.create "constr:appl_arg"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fa8c2a6f5..e089389fe 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -167,6 +167,7 @@ module Constr :
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
     val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
+    val record_declaration : constr_expr Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e051d1aad..33bc17624 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -71,6 +71,8 @@ let e_give_exact flags c gl =
     if occur_existential t1 or occur_existential t2 then 
       tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_check c) gl
     else exact_check c gl
+(*   let t1 = (pf_type_of gl c) in *)
+(*     tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl *)
       
 let assumption flags id = e_give_exact flags (mkVar id)
 
@@ -1242,7 +1244,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance binders instance fields = 
-  new_instance binders instance fields ~generalize:false None
+  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1251,17 +1253,17 @@ let require_library dirpath =
 let declare_instance_refl binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" 
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
+       [((dummy_loc,id_of_string "reflexivity"),lemma)]
 
 let declare_instance_sym binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "symmetry"),[],lemma)]
+       [((dummy_loc,id_of_string "symmetry"),lemma)]
 
 let declare_instance_trans binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" 
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "transitivity"),[],lemma)]
+       [((dummy_loc,id_of_string "transitivity"),lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
@@ -1286,16 +1288,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], lemma1);
-	       ((dummy_loc,id_of_string "PreOrder_Transitive"),[], lemma3)])
+	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
+	       ((dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) -> 
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PER_Symmetric"), [], lemma2);
-	       ((dummy_loc,id_of_string "PER_Transitive"),[], lemma3)])
+	      [((dummy_loc,id_of_string "PER_Symmetric"), lemma2);
+	       ((dummy_loc,id_of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) -> 
 	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
@@ -1303,9 +1305,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
 	  anew_instance binders instance 
-	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], lemma1);
-	     ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], lemma2);
-	     ((dummy_loc,id_of_string "Equivalence_Transitive"),[], lemma3)])
+	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
+	     ((dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
+	     ((dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
 
 type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1483,9 +1485,9 @@ let add_setoid binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance binders instance
-      [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkappc "Seq_refl" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], mkappc "Seq_sym" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkappc "Seq_trans" [a;aeq;t])])
+      [((dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       ((dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       ((dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 let add_morphism_infer m n =
   init_setoid ();
@@ -1520,7 +1522,7 @@ let add_morphism binders m s n =
 	     [cHole; s; m]))
   in	  
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-    ignore(new_instance binders instance []
+    ignore(new_instance binders instance (CRecord (dummy_loc,None,[]))
 	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
 	      None)
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 8da1c3176..c3a00259b 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -39,4 +39,4 @@ Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
 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))) [ I : ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8d40c19a5..40f1f96c3 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.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 *)
@@ -27,12 +26,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class DecidableSetoid A [ 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 (( 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
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 22d87829a..555f262ef 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -48,7 +48,7 @@ let _ =
 	Auto.add_hints false [typeclasses_db] 
 	  (Vernacexpr.HintsResolve 
 	      [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
-
+    
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
   let _, r = decompose_prod_assum instance in
@@ -71,196 +71,15 @@ type binder_list = (identifier located * bool * constr_expr) list
 
 (* Calls to interpretation functions. *)
 
-let interp_binders_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) ((loc, i), t) -> 
-      let n = Name i in
-      let t' = interp_binder_evars isevars env n t in
-      let d = (i,None,t') in
-	(push_named d env, i :: ids, d::params))
-    (env, avoid, []) l
-
-let interp_typeclass_context_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) (iid, bk, l) -> 
-      let t' = interp_binder_evars isevars env (snd iid) l in
-      let i = match snd iid with
-	| Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
-	| Name id -> id
-      in
-      let d = (i,None,t') in
-	(push_named d env, i :: ids, d::params))
-    (env, avoid, []) l
-
 let interp_type_evars evdref env ?(impls=([],[])) typ =
   let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
-
-let mk_interning_data env na impls typ =
-  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
-  in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
     
-let interp_fields_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> 
-      let impl, t' = interp_type_evars isevars env ~impls t in
-      let data = mk_interning_data env i impl t' in
-      let d = (Name i,None,t') in
-	(push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
-    (env, [], avoid, [], ([], [])) l    
-
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
 open Topconstr
-
-let implicits_of_context ctx =
-  list_map_i (fun i name ->
-    let explname = 
-      match name with 
-      | Name n -> Some n
-      | Anonymous -> None
-    in ExplByPos (i, explname), (true, true))
-    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-
-let name_typeclass_binder avoid = function
-  | LocalRawAssum ([loc, Anonymous], bk, c) ->
-      let name = 
-	let id = 
-	match c with
-	    CApp (_, (_, CRef (Ident (loc,id))), _) -> id
-	  | _ -> id_of_string "assum"
-	in Implicit_quantifiers.make_fresh avoid (Global.env ()) id
-      in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid
-  | x -> x, avoid
-
-let name_typeclass_binders avoid l = 
-  let l', avoid = 
-    List.fold_left 
-      (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in
-				   b' :: binders, avoid)
-      ([], avoid) l
-  in List.rev l', avoid
-      
-let new_class id par ar sup props =
-  let env0 = Global.env() in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in
-  let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in
-  let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in
-  let sup, bound = name_typeclass_binders bound sup in
-  let par, bound = name_typeclass_binders bound par in
-  let supnames = 
-    List.fold_left (fun acc b -> 
-      match b with
-      | LocalRawAssum (nl, _, _) -> nl @ acc
-      | LocalRawDef _ -> assert(false))
-      [] sup
-  in
-
-  (* Interpret the arity *)
-  let arity_imps, fullarity = 
-    let ar = 
-      match ar with
-	Some ar -> ar | None -> (dummy_loc, Rawterm.RType None)
-    in
-    let arity = CSort (fst ar, snd ar) in
-    let term = prod_constr_expr (prod_constr_expr arity par) sup in
-      interp_type_evars isevars env0 term      
-  in
-  let ctx_params, arity = decompose_prod_assum fullarity in
-  let env_params = push_rel_context ctx_params env0 in
-    
-  (* Interpret the definitions and propositions *)
-  let env_props, prop_impls, bound, ctx_props, _ = 
-    interp_fields_evars isevars env_params bound props 
-  in
-  let subs = List.map (fun ((loc, id), b, _) -> b) props in
-  (* Instantiate evars and check all are resolved *)
-  let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
-  let isevars = Typeclasses.resolve_typeclasses env_props isevars in
-  let sigma = Evd.evars_of isevars in
-  let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in
-  let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in
-  let arity = Reductionops.nf_evar sigma arity in
-  let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
-  let fieldimpls = 
-    (* Make the class and all params implicits in the projections *)
-    let ctx_impls = implicits_of_context ctx_params in
-    let len = succ (List.length ctx_params) in
-      List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
-  in
-  let impl, projs = 
-    let params = ctx_params and fields = ctx_props in
-      List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
-      match fields with
-      | [(Name proj_name, _, field)] ->
-	  let class_body = it_mkLambda_or_LetIn field params in
-	  let class_type = 
-	    match ar with
-	    | Some _ -> Some (it_mkProd_or_LetIn arity params)
-	    | None -> None
-	  in
-	  let class_entry = 
-	    { const_entry_body = class_body;
-	      const_entry_type = class_type;
-	      const_entry_opaque = false;
-	      const_entry_boxed = false }
-	  in
-	  let cst = Declare.declare_constant (snd id)
-	    (DefinitionEntry class_entry, IsDefinition Definition) 
-	  in
-	  let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
-	  let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
-	  let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
-	  let proj_entry = 
-	    { const_entry_body = proj_body;
-	      const_entry_type = Some proj_type;
-	      const_entry_opaque = false;
-	      const_entry_boxed = false }
-	  in
-	  let proj_cst = Declare.declare_constant proj_name
-	    (DefinitionEntry proj_entry, IsDefinition Definition) 
-	  in
-	  let cref = ConstRef cst in
-	    Impargs.declare_manual_implicits false cref arity_imps;
-	    Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
-	    set_rigid cst;
-	    cref, [proj_name, Some proj_cst]
-      | _ ->
-	  let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-	  let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	  let kn = Record.declare_structure true (snd id) idb arity_imps
-	    params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
-	  in
-	    IndRef (kn,0), (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
-			       (List.rev fields) (Recordops.lookup_projections (kn,0)))
-  in
-  let ctx_context =
-    List.map (fun (na, b, t) -> 
-      match Typeclasses.class_of_constr t with
-      | Some cl -> Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames)
-      | None -> None)
-      ctx_params, ctx_params
-  in
-  let k =
-    { cl_impl = impl;
-      cl_context = ctx_context;
-      cl_props = ctx_props;
-      cl_projs = projs }
-  in
-    List.iter2 (fun p sub -> 
-      if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
-      k.cl_projs subs;
-    add_class k
     
-type binder_def_list = (identifier located * identifier located list * constr_expr) list
-
-let binders_of_lidents l =
-  List.map (fun (loc, id) -> 
-    LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, 
-		  CHole (loc, Some (BinderType (Name id))))) l
-
 let type_ctx_instance isevars env ctx inst subst =
   let (s, _) = 
     List.fold_left2
@@ -362,29 +181,33 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
       end
     else
       begin
-	let subst = 
-	  let props = 
-	    List.map (fun (x, l, d) -> 
-	      x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
-	      props
-	  in
-	    if List.length props > List.length k.cl_props then 
-	      mismatched_props env' (List.map snd props) k.cl_props;
-	    let props, rest = 
-	      List.fold_left
-		(fun (props, rest) (id,_,_) -> 
-		  try 
-		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
-		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		      Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
-		      c :: props, rest'
-		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
-		([], props) k.cl_props
-	    in
-	      if rest <> [] then 
-		unbound_method env' k.cl_impl (fst (List.hd rest))
-	      else
-		type_ctx_instance isevars env' k.cl_props props substctx
+	let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in
+	  if List.length props > List.length k.cl_props then 
+	    mismatched_props env' (List.map snd props) k.cl_props;
+	  let subst = 
+	    match k.cl_props with 
+	    | [(na,b,ty)] -> 
+		let term = match props with [] -> CHole (Util.dummy_loc, None) 
+		  | [(_,f)] -> f | _ -> assert false in
+		let ty' = substl subst ty in
+		let c = interp_casted_constr_evars isevars env' term ty' in
+		  c :: subst
+	    | _ ->
+		let props, rest = 
+		  List.fold_left
+		    (fun (props, rest) (id,_,_) -> 
+		      try 
+			let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+			let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
+			  Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+			  c :: props, rest'
+		      with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+		    ([], props) k.cl_props
+		in
+		  if rest <> [] then 
+		    unbound_method env' k.cl_impl (fst (List.hd rest))
+		  else
+		    type_ctx_instance isevars env' k.cl_props props substctx
 	in
 	let app, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 4f20f1649..c79eccab8 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -29,24 +29,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
-type binder_list = (identifier located * bool * constr_expr) list
-type binder_def_list = (identifier located * identifier located list * constr_expr) list
- 
-val binders_of_lidents : identifier located list -> local_binder list
-
-val name_typeclass_binders : Idset.t ->
-    Topconstr.local_binder list ->
-    Topconstr.local_binder list * Idset.t
-
-(* val declare_implicit_proj : typeclass -> (identifier * constant) ->  *)
-(*   Impargs.manual_explicitation list -> bool -> unit *)
-
-val new_class : identifier located ->
-  local_binder list ->
-  Vernacexpr.sort_expr located option ->
-  local_binder list ->
-  binder_list -> unit
-
 (* Instance declaration *)
 
 val declare_instance : bool -> identifier located -> unit
@@ -66,7 +48,7 @@ val new_instance :
   ?global:bool -> (* Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
-  binder_def_list ->
+  constr_expr ->
   ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
   ?hook:(constant -> unit) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5cccc225c..47c51b83f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -528,7 +528,9 @@ let interp_mutual paramsl indl notations finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
-  let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in
+  let (env_params, ctx_params), userimpls = 
+    interp_context_evars ~fail_anonymous:false evdref env0 paramsl 
+  in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -622,7 +624,7 @@ let prepare_inductive ntnl indl =
   let indl =
     List.map (fun ((_,indname),_,ar,lc) -> { 
       ind_name = indname;
-      ind_arity = ar;
+      ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
       ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
     }) indl in
   List.fold_right Option.List.cons ntnl [], indl
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 386663538..8ccaaed35 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -67,7 +67,7 @@ val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_ty
 val check_mutuality : Environ.env -> definition_object_kind ->
   (identifier * types) list -> unit
 
-val build_mutual : ((lident * local_binder list * constr_expr * constructor_expr list) * 
+val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * 
 		                decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5ebd89789..c066bae5c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -64,16 +64,19 @@ let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
-  let (env1,newps), imps = interp_context Evd.empty env0 ps in
-  let fullarity = it_mkProd_or_LetIn t newps in
-  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
+  let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
+  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar nots (binders_of_decls fs)
   in
-  let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in
-  let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in
-  let ce t = Evarutil.check_evars env0 Evd.empty !evars t in
+  let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
+  let evars = Typeclasses.resolve_typeclasses env_ar evars in
+  let sigma = Evd.evars_of evars in
+  let newps = Evarutil.nf_rel_context_evar sigma newps in
+  let newfs = Evarutil.nf_rel_context_evar sigma newfs in
+  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps;
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs;
     imps, newps, impls, newfs
@@ -242,11 +245,105 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field
   let build = ConstructRef (rsp,1) in
     if is_coe then Class.try_add_new_coercion build Global;
     Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
-    kn
+    kn,0
+
+let implicits_of_context ctx =
+  list_map_i (fun i name ->
+    let explname = 
+      match name with 
+      | Name n -> Some n
+      | Anonymous -> None
+    in ExplByPos (i, explname), (true, true))
+    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+
+open Typeclasses
+
+let typeclasses_db = "typeclass_instances"
+
+let qualid_of_con c = 
+  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+
+let set_rigid c = 
+  Auto.add_hints false [typeclasses_db] 
+    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
+
+let declare_instance_cst glob con =
+  let instance = Typeops.type_of_constant (Global.env ()) con in
+  let _, r = Sign.decompose_prod_assum instance in
+    match class_of_constr r with
+      | 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
+    ?(kind=StructureComponent) ?name is_coe coers =
+  let fieldimpls = 
+    (* Make the class and all params implicits in the projections *)
+    let ctx_impls = implicits_of_context params in
+    let len = succ (List.length params) in
+      List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls
+  in
+  let impl, projs =
+    match fields with
+    | [(Name proj_name, _, field)] ->
+	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 =
+	  { const_entry_body = class_body;
+	    const_entry_type = class_type;
+	    const_entry_opaque = false;
+	    const_entry_boxed = false }
+	in
+	let cst = Declare.declare_constant (snd id)
+	  (DefinitionEntry class_entry, IsDefinition Definition) 
+	in
+	let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
+	let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
+	let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+	let proj_entry = 
+	  { const_entry_body = proj_body;
+	    const_entry_type = Some proj_type;
+	    const_entry_opaque = false;
+	    const_entry_boxed = false }
+	in
+	let proj_cst = Declare.declare_constant proj_name
+	  (DefinitionEntry proj_entry, IsDefinition Definition) 
+	in
+	let cref = ConstRef cst in
+	  Impargs.declare_manual_implicits false cref paramimpls;
+	  Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+	  set_rigid cst; (* set_rigid proj_cst; *)
+	  cref, [proj_name, Some proj_cst]
+    | _ ->
+	let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	let ind = declare_structure true (snd id) idbuild paramimpls
+	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
+	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+	in
+	  (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *)
+	  IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
+			     (List.rev fields) (Recordops.lookup_projections ind))
+  in
+  let ctx_context =
+    List.map (fun (na, b, t) -> 
+      match Typeclasses.class_of_constr t with
+      | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+      | None -> None)
+      params, params
+  in
+  let k =
+    { cl_impl = impl;
+      cl_context = ctx_context;
+      cl_props = fields;
+      cl_projs = projs }
+  in
+    List.iter2 (fun p sub -> 
+      if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
+      k.cl_projs coers;
+    add_class k; impl
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
-let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let coers,fs = List.split cfs in
   let extract_name acc = function
@@ -256,11 +353,14 @@ let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
+  let sc = Option.map mkSort s in
   let implpars, params, implfs, fields = 
     States.with_heavy_rollback (fun () ->
-      typecheck_params_and_fields idstruc (mkSort s) ps notations fs) ()
+      typecheck_params_and_fields idstruc sc ps notations fs) ()
   in
-  let implfs = 
-    List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
-  in declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
-      
+    if kind then
+      let arity = Option.cata (fun x -> x) (new_Type ()) sc in
+      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)
+    else declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 7aea948f3..57d8cccc0 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -15,6 +15,7 @@ open Sign
 open Vernacexpr
 open Topconstr
 open Impargs
+open Libnames
 (*i*)
 
 (* [declare_projections ref name coers params fields] declare projections of
@@ -27,14 +28,13 @@ val declare_projections :
   (name * bool) list * constant option list
 
 val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> 
-  manual_explicitation list -> rel_context -> (* params *)
-  Term.constr -> (* arity *)
+  manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
   Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
   bool -> (* coercion? *)
   bool list -> (* field coercions *)
-  mutual_inductive
+  inductive
 
 val definition_structure :
-  bool (*coinductive?*)*lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion with_notation) list * identifier * sorts -> kernel_name
+  bool (* structure or class *) * bool (*coinductive?*)*lident with_coercion * local_binder list *
+  (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 504561100..4b4f7abb5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -372,26 +372,27 @@ let vernac_assumption kind l nl=
 	  else Dumpglob.dump_definition lid true "var") idl;
       declare_assumption idl is_coe kind [] c false false nl) l
 	  
-let vernac_record finite struc binders sort nameopt cfs =
+let vernac_record k finite struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
 	Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
-  let s = interp_constr sigma env sort in
-  let s = Reductionops.whd_betadeltaiota env sigma s in
-  let s = match kind_of_term s with
-    | Sort s -> s
-    | _ -> user_err_loc
-        (constr_loc sort,"definition_structure", str "Sort expected.") in
+  let s = Option.map (fun x ->
+    let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in
+      match kind_of_term s with
+      | Sort s -> s
+      | _ -> user_err_loc
+          (constr_loc x,"definition_structure", str "Sort expected.")) sort
+  in
     if Dumpglob.dump () then (
       Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun ((_, x), _) ->
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (finite,struc,binders,cfs,const,s))
+    ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s))
       
 let vernac_inductive finite indl = 
   if Dumpglob.dump () then
@@ -404,16 +405,16 @@ let vernac_inductive finite indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( id , bl , c ,RecordDecl (oc,fs) ), None ] -> 
-            vernac_record finite (false,id) bl c oc fs
+  | [ ( id , bl , c ,RecordDecl (b,oc,fs) ), None ] -> 
+      vernac_record b finite (false,id) bl c oc fs
   | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> 
-            Util.error "where clause not supported for (co)inductive records"
+      Util.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function 
-              | ( 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
-            Command.build_mutual indl finite
+      | ( 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
+      Command.build_mutual indl finite
 
 let vernac_fixpoint l b = 
   if Dumpglob.dump () then
@@ -609,11 +610,6 @@ let vernac_identity_coercion stre id qids qidt =
   Class.try_add_new_identity_coercion id stre source target
 
 (* Type classes *)
-let vernac_class id par ar sup props =
-  if Dumpglob.dump () then (
-      Dumpglob.dump_definition id false "class";
-      List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props);
-  Classes.new_class id par ar sup props
  
 let vernac_instance glob sup inst props pri =
   Dumpglob.dump_constraint inst false "inst";
@@ -1327,7 +1323,7 @@ let interp c = match c with
 
   | VernacEndSegment lid -> vernac_end_segment lid
 
-  | VernacRecord ((_,finite),id,bl,s,idopt,fs) -> vernac_record finite id bl s idopt fs
+  | 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
@@ -1335,7 +1331,7 @@ 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
+(*   | 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
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2727100bf..8addcd3ca 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -163,9 +163,9 @@ 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 lident option * local_decl_expr with_coercion with_notation list
+  | RecordDecl of bool * lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-  lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr
+  lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast
 
@@ -216,9 +216,9 @@ type vernac_expr =
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
-  | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *)
+  | VernacRecord of (bool*bool) (* = Structure or Class * Inductive or CoInductive *)
       * lident with_coercion * local_binder list
-      * constr_expr * lident option * local_decl_expr with_coercion with_notation list
+      * constr_expr option * lident option * local_decl_expr with_coercion with_notation list
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
@@ -230,18 +230,18 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
 
   (* Type classes *)
-  | VernacClass of
-      lident * (* name *)
-	local_binder list * (* params *)
-	sort_expr located option * (* arity *)
-	local_binder list * (* constraints *)
-	(lident * bool * constr_expr) list (* props, with substructure hints *)
+(*   | VernacClass of *)
+(*       lident * (\* name *\) *)
+(* 	local_binder list * (\* params *\) *)
+(* 	sort_expr located option * (\* arity *\) *)
+(* 	local_binder list * (\* constraints *\) *)
+(* 	(lident * bool * constr_expr) list (\* props, with substructure hints *\) *)
 	
   | VernacInstance of
       bool * (* global *)
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
-	(lident * lident list * constr_expr) list * (* props *)
+	constr_expr * (* props *)
 	int option (* Priority *)
 
   | VernacContext of local_binder list