Do another pass on the typeclasses code. Correct globalization of class

names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code. 
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class. 
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].


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

23 files changed, 404 insertions, 422 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index a2184a557e..39865f1f9f 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -108,11 +108,8 @@ let new_instance ctx (instid, bk, cl) props pri =
   let tclass =
     match bk with
       | Explicit ->
-	  let id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = 
-	    try class_info (snd id)
-	    with Not_found -> unbound_class env id
-	  in
+	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
+	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
 	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
 	    if needlen <> applen then 
@@ -129,7 +126,7 @@ let new_instance ctx (instid, bk, cl) props pri =
 		      in t, avoid
 		  | None -> failwith ("new instance: under-applied typeclass"))
 	      par (List.rev k.cl_context)
-	    in Topconstr.CAppExpl (Util.dummy_loc, (None, Ident id), pars)
+	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
       | Implicit -> cl
   in
@@ -143,13 +140,8 @@ let new_instance ctx (instid, bk, cl) props pri =
     let c = Command.generalize_constr_expr tclass ctx in
     let c' = interp_type_evars isevars env c in
     let ctx, c = Classes.decompose_named_assum c' in
-      (match kind_of_term c with 
-	  App (c, args) -> 
-	    let cl = Option.get (class_of_constr c) in
-	      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
-	| _ -> 
-	    let cl = Option.get (class_of_constr c) in
-	      cl, ctx, [])
+    let cl, args = Typeclasses.dest_class_app c in
+      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -159,7 +151,7 @@ let new_instance ctx (instid, bk, cl) props pri =
 	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
 	    id
       | Anonymous -> 
-	  let i = Nameops.add_suffix k.cl_name "_instance_0" in
+	  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' = Classes.push_named_context ctx' env in
@@ -187,18 +179,17 @@ let new_instance ctx (instid, bk, cl) props pri =
 	  ([], props) k.cl_props
       in
 	if rest <> [] then 
-	  unbound_method env' k.cl_name (fst (List.hd rest))
+	  unbound_method env' k.cl_impl (fst (List.hd rest))
 	else
 	  type_ctx_instance isevars env' k.cl_props props substctx
   in
-  let app = 
-    applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
-  in 
+  let inst_constr, ty_constr = instance_constructor k in
+  let app = inst_constr (List.rev_map snd subst) in 
   let term = it_mkNamedLambda_or_LetIn app ctx' in
   isevars := Evarutil.nf_evar_defs !isevars;
   let term = Evarutil.nf_isevar !isevars term in
   let termtype = 
-    let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
+    let app = applistc ty_constr (List.rev_map snd substctx) in
     let t = it_mkNamedProd_or_LetIn app ctx' in
       Evarutil.nf_isevar !isevars t
   in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8a0b940b1a..3b2b5d3d43 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -159,12 +159,12 @@ let compute_context_vars env l =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+    | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
     | _ -> raise Not_found
-
+      
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, l
+    | CApp (loc, (None,CRef ref), l) -> loc, ref, l
     | _ -> raise Not_found
 
 let full_class_binders env l = 
@@ -173,12 +173,13 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Explicit -> 
-	    let (id, l) = destClassAppExpl cl in
+	    let (loc, id, l) = destClassAppExpl cl in
+	    let gr = Nametab.global id in
 	      (try
-		  let c = class_info (snd id) in
+		  let c = class_info gr in
 		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
-		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
-		with Not_found -> unbound_class (Global.env ()) id)
+		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
+		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
 	| Implicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 4ea95fc43c..9ecdcd6c07 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -20,12 +20,13 @@ open Mod_subst
 open Rawterm
 open Topconstr
 open Util
+open Libnames
 open Typeclasses
 (*i*)
 
 val ids_of_list : identifier list -> Idset.t
-val destClassApp : constr_expr -> identifier located * constr_expr list
-val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> loc * reference * constr_expr list
+val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
 
 val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
@@ -55,10 +56,10 @@ val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  ((Names.identifier * bool) option * Term.named_declaration) list ->
+  ((global_reference * bool) option * Term.named_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index b39cdeddab..767072e2bb 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -763,7 +763,7 @@ let print_canonical_projections () =
 open Typeclasses
 
 let pr_typeclass env t = 
-  gallina_print_inductive (fst t.cl_impl)
+  print_ref false t.cl_impl
 
 let print_typeclasses () =
   let env = Global.env () in
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index c6478376d6..db1d8bb109 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -60,7 +60,7 @@ val print_canonical_projections : unit -> std_ppcmds
 
 (* Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> std_ppcmds
-val print_instances : reference -> std_ppcmds
+val print_instances : global_reference -> std_ppcmds
 
 
 val inspect : int -> std_ppcmds
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 3406d06aa4..0d462f793d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -141,13 +141,16 @@ let clenv_conv_leq env sigma t c bound =
   check_evars env sigma evars (applist (c,args));
   args
 
-let mk_clenv_from_n gls n (c,cty) =
-  let evd = create_goal_evar_defs gls.sigma in
+let mk_clenv_from_env environ sigma n (c,cty) =
+  let evd = create_goal_evar_defs sigma in
   let (env,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     evd = env;
-    env = Global.env_of_context gls.it.evar_hyps }
+    env = environ }
+
+let mk_clenv_from_n gls n (c,cty) =
+  mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 1697bb3c2b..6a7038a078 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -54,6 +54,7 @@ val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_from_n :
   evar_info sigma -> int option -> constr * types -> clausenv
 val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
 (***************************************************************)
 (* linking of clenvs *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 47be844600..9d837df0ee 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,22 +30,22 @@ type rels = constr list
 
 (* This module defines type-classes *)
 type typeclass = {
-  (* Name of the class. FIXME: should not necessarily be globally unique. *)
-  cl_name : identifier;
+  (* The class implementation *)
+  cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : ((identifier * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * named_declaration) list; 
 
   cl_params: int;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : named_context;
-
-  (* The class implementation: a record parameterized by the context with defs in it. *)
-  cl_impl : inductive; 
+  
+  (* The method implementaions as projections. *)
+  cl_projs : constant list;
 }
 
-type typeclasses = (identifier, typeclass) Gmap.t
+type typeclasses = (global_reference, typeclass) Gmap.t
 
 type instance = {
   is_class: typeclass;
@@ -53,11 +53,11 @@ type instance = {
   is_impl: constant; 
 }
 
-type instances = (identifier, instance list) Gmap.t
+type instances = (global_reference, instance list) Gmap.t
     
 let classes : typeclasses ref = ref Gmap.empty
 
-let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty
+let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty
   
 let instances : instances ref = ref Gmap.empty
   
@@ -124,47 +124,64 @@ open Libobject
 let subst (_,subst,(cl,m,inst)) = 
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst c = Mod_subst.subst_mps subst c
-  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+  and do_subst_gr gr = fst (subst_global subst gr)
   in
   let do_subst_named ctx = 
-    List.map (fun (na, b, t) ->
+    list_smartmap (fun (na, b, t) ->
       (na, Option.smartmap do_subst b, do_subst t))
       ctx
   in
   let do_subst_ctx ctx = 
-    List.map (fun (cl, (na, b, t)) ->
-      (cl, (na, Option.smartmap do_subst b, do_subst t)))
+    list_smartmap (fun (cl, (na, b, t)) ->
+      (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl,
+      (na, Option.smartmap do_subst b, do_subst t)))
       ctx
   in
-  let subst_class cl = 
-    let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl;
+  let do_subst_projs projs = list_smartmap do_subst_con projs in
+  let subst_class k cl classes = 
+    let k = do_subst_gr k in
+    let cl' = { cl with cl_impl = k;
 		cl_context = do_subst_ctx cl.cl_context;
-		cl_props = do_subst_named cl.cl_props; }
-    in if cl' = cl then cl else cl'
+		cl_props = do_subst_named cl.cl_props;
+		cl_projs = do_subst_projs cl.cl_projs; }
+    in 
+    let cl' = if cl' = cl then cl else cl' in
+      Gmap.add k cl' classes
   in
-  let subst_inst classes insts =
-    List.map (fun is -> 
-      let is' = 
-	{ is_class = Gmap.find is.is_class.cl_name classes; 
-	  is_pri = is.is_pri;
-	  is_impl = do_subst_con is.is_impl }
-      in if is' = is then is else is') insts
+  let classes = Gmap.fold subst_class cl Gmap.empty in
+  let subst_inst k insts instances =
+    let k = do_subst_gr k in
+    let cl = Gmap.find k classes in
+    let insts' = 
+      list_smartmap (fun is -> 
+	let is' = 
+	  { is_class = cl; 
+	    is_pri = is.is_pri;
+	    is_impl = do_subst_con is.is_impl }
+	in if is' = is then is else is') insts
+    in  Gmap.add k insts' instances
   in
-  let classes = Gmap.map subst_class cl in
-  let instances = Gmap.map (subst_inst classes) inst in
+  let instances = Gmap.fold subst_inst inst Gmap.empty in
     (classes, m, instances)
 
 let discharge (_,(cl,m,inst)) =
-  let subst_class cl = 
-    { cl with cl_impl = Lib.discharge_inductive cl.cl_impl }
+  let discharge_named (cl, r) =
+    Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r
   in
-  let subst_inst classes insts =
-    List.map (fun is -> { is_impl = Lib.discharge_con is.is_impl;
-			  is_pri = is.is_pri;
-			  is_class = Gmap.find is.is_class.cl_name classes; }) insts
+  let subst_class cl = 
+    { cl with cl_impl = Lib.discharge_global cl.cl_impl;
+      cl_context = list_smartmap discharge_named cl.cl_context;
+      cl_projs = list_smartmap Lib.discharge_con cl.cl_projs }
   in
   let classes = Gmap.map subst_class cl in
-  let instances = Gmap.map (subst_inst classes) inst in
+  let subst_inst insts =
+    List.map (fun is ->
+      { is_impl = Lib.discharge_con is.is_impl;
+	is_pri = is.is_pri;
+	is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; })
+      insts
+  in
+  let instances = Gmap.map subst_inst inst in
     Some (classes, m, instances)
   
 let (input,output) = 
@@ -181,24 +198,20 @@ let (input,output) =
 let update () = 
   Lib.add_anonymous_leaf (input (!classes, !methods, !instances))
 
-let class_methods cl =
-  List.map (function (x, _, _) -> x) cl.cl_props
-
 let add_class c = 
-  classes := Gmap.add c.cl_name c !classes;
-  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c);
+  classes := Gmap.add c.cl_impl c !classes;
+  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_impl acc) !methods c.cl_projs;
   update ()
     
 let class_info c = 
-  Gmap.find c !classes
+  try Gmap.find c !classes
+  with _ -> not_a_class (Global.env()) (constr_of_global c)
 
-let class_of_inductive ind = 
-  let res = Gmap.fold 
-    (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc)
-    !classes None
-  in match res with
-      None -> raise Not_found
-    | Some cl -> cl
+let instance_constructor cl = 
+  match cl.cl_impl with
+    | IndRef ind -> (fun args -> applistc (mkConstruct (ind, 1)) args), mkInd ind
+    | ConstRef cst -> list_last, mkConst cst
+    | _ -> assert false
 
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
 
@@ -210,25 +223,16 @@ let gmapl_add x y m =
     Gmap.add x [y] m
 
 let instances_of c = 
-  try Gmap.find c.cl_name !instances with Not_found -> []
+  try Gmap.find c.cl_impl !instances with Not_found -> []
 
 let add_instance i =
-  try
-    let cl = Gmap.find i.is_class.cl_name !classes in
-      instances := gmapl_add cl.cl_name { i with is_class = cl } !instances;
-      add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
-      update ()
-  with Not_found -> unbound_class (Global.env ()) (dummy_loc, i.is_class.cl_name)
-
-open Libnames
-      
-let id_of_reference r = 
-  let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id
+  let cl = Gmap.find i.is_class.cl_impl !classes in
+    instances := gmapl_add cl.cl_impl { i with is_class = cl } !instances;
+    add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
+    update ()
 
 let instances r = 
-  let id = id_of_reference r in
-    try let cl = class_info id in instances_of cl
-    with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
+  let cl = class_info r in instances_of cl
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
 let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false)
@@ -273,12 +277,11 @@ let resolve_one_typeclass_evd env evd types =
 let method_typeclass ref = 
   match ref with 
     | ConstRef c -> 
-	let (_, _, l) = Names.repr_con c in
-	  class_info (Gmap.find (Names.id_of_label l) !methods)
+	class_info (Gmap.find c !methods)
     | _ -> raise Not_found
       
-let is_class ind = 
-  Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false
+let is_class gr = 
+  Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
   
 let is_implicit_arg k = 
   match k with
@@ -332,14 +335,18 @@ let is_independent evm ev =
 (*   in sat (Evarutil.nf_evar_defs evd) *)
   
 let class_of_constr c = 
-  let extract_ind c =
-    match kind_of_term c with
-	Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
-      | _ -> None
+  let extract_cl c =
+    try Some (class_info (global_of_constr c)) with _ -> None
   in
     match kind_of_term c with
-	App (c, _) -> extract_ind c
-      | _ -> extract_ind c
+	App (c, _) -> extract_cl c
+      | _ -> extract_cl c
+
+let dest_class_app c =
+  let cl c = class_info (global_of_constr c) in
+    match kind_of_term c with
+	App (c, args) -> cl c, args
+      | _ -> cl c, [||]
 
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index dba60234bc..193f3ae3c2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -24,20 +24,21 @@ open Util
 
 (* This module defines type-classes *)
 type typeclass = {
-  (* Name of the class. FIXME: should not necessarily be globally unique. *)
-  cl_name : identifier;
+  (* The class implementation: a record parameterized by the context with defs in it or a definition if 
+     the class is a singleton. This acts as the classe's global identifier. *)
+  cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the 
      typeclass argument is a direct superclass. *)
-  cl_context : ((identifier * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * named_declaration) list; 
 
   cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : named_context;
 
-  (* The class implementation: a record parameterized by the context with defs in it. *)
-  cl_impl : inductive; 
+  (* The methods implementations of the typeclass as projections. *)
+  cl_projs : constant list;
 }
 
 type instance = {
@@ -46,7 +47,7 @@ type instance = {
   is_impl: constant;
 }
   
-val instances : Libnames.reference -> instance list
+val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list
 val add_class : typeclass -> unit
 val add_instance : instance -> unit
@@ -54,16 +55,16 @@ val add_instance : instance -> unit
 val register_add_instance_hint : (reference -> int option -> unit) -> unit
 val add_instance_hint : reference -> int option -> unit
 
-val class_info : identifier -> typeclass (* raises Not_found *)
-val class_of_inductive : inductive -> typeclass (* raises Not_found *)
+val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
+val is_class : global_reference -> bool
+val class_of_constr : constr -> typeclass option
+val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
+
+(* Returns the constructor for the given fields of the class and the type constructor. *)
+val instance_constructor : typeclass -> (constr list -> constr) * types
 
 val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
 val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
-
-val is_class : inductive -> bool
-
-val class_of_constr : constr -> typeclass option
-
 val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
 
 (* Use evar_extra for marking resolvable evars. *)
@@ -88,9 +89,15 @@ val nf_substitution : evar_map -> substitution -> substitution
 
 val is_implicit_arg : hole_kind -> bool
 
+val qualid_of_con : Names.constant -> Libnames.reference
 
-val subst :  'a * Mod_subst.substitution *
-    ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) ->
-    (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t
 
-val qualid_of_con : Names.constant -> Libnames.reference
+(* debug *)
+
+(* val subst :  *)
+(*     'a * Mod_subst.substitution * *)
+(*     ((Libnames.global_reference, typeclass) Gmap.t * 'b * *)
+(*      ('c, instance list) Gmap.t) -> *)
+(*     (Libnames.global_reference, typeclass) Gmap.t * 'b * *)
+(*     ('c, instance list) Gmap.t *)
+
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 980f327cb5..1648f667ab 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -19,13 +19,14 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
+open Libnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | UnboundClass of identifier located
-    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NotAClass of constr
+    | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
@@ -33,7 +34,7 @@ exception TypeClassError of env * typeclass_error
 
 let typeclass_error env err = raise (TypeClassError (env, err))
 
-let unbound_class env id = typeclass_error env (UnboundClass id)
+let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fbc2f25449..82e37f41d8 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -19,21 +19,22 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
+open Libnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | UnboundClass of identifier located
-    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NotAClass of constr
+    | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
-val unbound_class : env -> identifier located -> 'a
+val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> identifier -> identifier located -> 'a
+val unbound_method : env -> global_reference -> identifier located -> 'a
 
 val no_instance : env -> identifier located -> constr list -> 'a
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index dd552845dc..4edb8191e2 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -36,7 +36,7 @@ open Classes
 open Topconstr
 open Pfedit
 open Command
-
+open Libnames
 open Evd
 
 (** Typeclasses instance search tactic / eauto *)
@@ -418,12 +418,10 @@ END
 
 (** Typeclass-based rewriting. *)
 
-let morphism_class = lazy (class_info (id_of_string "Morphism"))
+let morphism_class = 
+  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))))
 
-let get_respect cl = 
-  Option.get (List.hd (Recordops.lookup_projections cl.cl_impl))
-
-let respect_proj = lazy (get_respect (Lazy.force morphism_class))
+let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs))
 
 let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s
 let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
@@ -433,14 +431,14 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
 let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
 
-let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive")
-let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive")
+let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive")
+let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexivity")
 
-let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric")
-let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric")
+let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric")
+let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetry")
 
-let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive")
-let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
+let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
+let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitivity")
 
 let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
 let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
@@ -474,7 +472,7 @@ let arrow_morphism a b =
 let setoid_refl pars x = 
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
       
-let morphism_class_proj = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
+let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl)
 
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
@@ -539,7 +537,6 @@ let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
 let transitive_proof env = find_class_proof transitive_type transitive_proof env
 
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
-  let (morphism_cl, morphism_proj) = Lazy.force morphism_class_proj in
   let morph_instance, proj, sigargs, m', args, args' = 
 (*     if is_equiv env sigma m then  *)
 (*       let params, rest = array_chop 3 args in *)
@@ -566,10 +563,10 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
     let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in
     let signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a, r) -> r) in
     let cl_args = [| appmtype ; signature ; appm |] in
-    let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
+    let app = mkApp (Lazy.force morphism_type, cl_args) in
     let morph = Evarutil.e_new_evar evars env app in
     let proj = 
-      mkApp (mkConst morphism_proj, 
+      mkApp (Lazy.force respect_proj, 
 	    Array.append cl_args [|morph|])
     in
       morph, proj, sigargs, appm, morphobjs, morphobjs'
@@ -605,9 +602,9 @@ type hypinfo = {
   abs : (constr * types) option;
 }
 
-let decompose_setoid_eqhyp gl c left2right =
-  let ctype = pf_type_of gl c in
-  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
+let decompose_setoid_eqhyp env sigma c left2right =
+  let ctype = Typing.type_of env sigma c in
+  let eqclause  = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
   let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
@@ -652,7 +649,15 @@ let rewrite2_unif_flags = {
 
 let allowK = true
 
-let unify_eqn gl hypinfo t = 
+let refresh_hypinfo env sigma hypinfo = 
+  let {l2r=l2r; c = c} = !hypinfo in
+    match c with 
+      | Some c ->
+	  (* Refresh the clausenv to not get the same meta twice in the goal. *)
+	  hypinfo := decompose_setoid_eqhyp env sigma c l2r;
+      | _ -> ()
+	  
+let unify_eqn env sigma hypinfo t = 
   try 
     let {cl=cl; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
     let env' = 
@@ -665,27 +670,21 @@ let unify_eqn gl hypinfo t =
     let c1 = Clenv.clenv_nf_meta env' c1 
     and c2 = Clenv.clenv_nf_meta env' c2
     and rel = Clenv.clenv_nf_meta env' rel in
-    let car = pf_type_of gl c1 in
+    let car = Typing.type_of env'.env (Evd.evars_of env'.evd) c1 in
     let prf =
       if abs = None then
 (* 	let (rel, args) = destApp typ in *)
 (* 	let relargs, args = array_chop (Array.length args - 2) args in *)
 (* 	let rel = mkApp (rel, relargs) in *)
 	let prf = Clenv.clenv_value env' in
-	  begin
-	    match c with 
-	      | Some c when occur_meta prf ->
-		  (* Refresh the clausenv to not get the same meta twice in the goal. *)
-		  hypinfo := decompose_setoid_eqhyp gl c l2r;
-	      | _ -> ()
-	  end;
+	  if occur_meta prf then refresh_hypinfo env sigma hypinfo;
 	  prf
       else prf
     in
     let res =
       if l2r then (prf, (car, rel, c1, c2))
       else
-	try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
+	try (mkApp (symmetric_proof env car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
 	with Not_found ->
 	  (prf, (car, mkApp (Lazy.force inverse, [| car ; rel |]), c2, c1))
     in Some (env', res)
@@ -705,7 +704,7 @@ let unfold_id t =
 let build_new gl env sigma occs hypinfo concl cstr evars =
   let is_occ occ = occs = [] || List.mem occ occs in
   let rec aux env t occ cstr =
-    match unify_eqn gl hypinfo t with
+    match unify_eqn env sigma hypinfo t with
       | Some (env', (prf, hypinfo as x)) ->
 	  if is_occ occ then (
 	    evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd));
@@ -755,6 +754,7 @@ let build_new gl env sigma occs hypinfo concl cstr evars =
 		  
 	    | Lambda (n, t, b) ->
 		let env' = Environ.push_rel (n, None, t) env in
+		refresh_hypinfo env' sigma hypinfo;
 		let b', occ = aux env' b occ None in
 		let res =
 		  match b' with
@@ -849,7 +849,7 @@ let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl =
 	  
 let cl_rewrite_clause c left2right occs clause gl =
   let meta = Evarutil.new_meta() in
-  let hypinfo = ref (decompose_setoid_eqhyp gl c left2right) in
+  let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in
     cl_rewrite_clause_aux hypinfo meta occs clause gl
 
 open Genarg
@@ -954,7 +954,7 @@ END
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
 
 let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit,
-				  CApp (dummy_loc, (None, mkIdentC (id_of_string s)), 
+				  CApp (dummy_loc, (None, mkRefC (Qualid (dummy_loc, qualid_of_string s))), 
 					[(a,None);(aeq,None)]))
 
 let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ())
@@ -973,19 +973,19 @@ let init_setoid () =
   check_required_library ["Coq";"Setoids";"Setoid"]
 
 let declare_instance_refl a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive" 
+  let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.reflexive" 
   in anew_instance instance 
-       [((dummy_loc,id_of_string "reflexive"),[],lemma)]
+       [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
 
 let declare_instance_sym a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_sym") "Symmetric" 
+  let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.symmetric"
   in anew_instance instance 
-       [((dummy_loc,id_of_string "symmetric"),[],lemma)]
+       [((dummy_loc,id_of_string "symmetry"),[],lemma)]
 
 let declare_instance_trans a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_trans") "Transitive" 
+  let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.transitive" 
   in anew_instance instance 
-       [((dummy_loc,id_of_string "transitive"),[],lemma)]
+       [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
 
@@ -993,7 +993,7 @@ let declare_relation a aeq n refl symm trans =
   init_setoid ();
   match (refl,symm,trans) with 
       (None, None, None) -> 
-	let instance = declare_instance a aeq n "DefaultRelation" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" 
 	in ignore(anew_instance instance [])
     | (Some lemma1, None, None) -> 
 	ignore (declare_instance_refl a aeq n lemma1)
@@ -1007,7 +1007,7 @@ let declare_relation a aeq n refl symm trans =
     | (Some lemma1, None, Some lemma3) -> 
 	let lemma_refl = declare_instance_refl a aeq n lemma1 in
 	let lemma_trans = declare_instance_trans a aeq n lemma3 in
-	let instance = declare_instance a aeq n "PreOrder" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
 	    anew_instance instance 
 	      [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl);
@@ -1015,7 +1015,7 @@ let declare_relation a aeq n refl symm trans =
     | (None, Some lemma2, Some lemma3) -> 
 	let lemma_sym = declare_instance_sym a aeq n lemma2 in
 	let lemma_trans = declare_instance_trans a aeq n lemma3 in
-	let instance = declare_instance a aeq n "PER" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
 	    anew_instance instance 
 	      [((dummy_loc,id_of_string "per_sym"),  [], mkIdentC lemma_sym);
@@ -1024,7 +1024,7 @@ let declare_relation a aeq n refl symm trans =
 	let lemma_refl = declare_instance_refl a aeq n lemma1 in 
 	let lemma_sym = declare_instance_sym a aeq n lemma2 in
 	let lemma_trans = declare_instance_trans a aeq n lemma3 in
-	let instance = declare_instance a aeq n "Equivalence" 
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
 	    anew_instance instance 
 	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
@@ -1075,7 +1075,7 @@ let respect_projection r ty =
   let ctx, inst = Sign.decompose_prod_assum ty in
   let mor, args = destApp inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
-  let app = mkApp (mkConst (Lazy.force respect_proj), 
+  let app = mkApp (Lazy.force respect_proj, 
 		  Array.append args [| instarg |]) in
     it_mkLambda_or_LetIn app ctx
       
@@ -1131,7 +1131,7 @@ let build_morphism_signature m =
     evars
   in
   let morph = 
-    mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sig_; m |])
+    mkApp (Lazy.force morphism_type, [| t; sig_; m |])
   in
   let evd = resolve_all_evars_once false (true, 15) env
     (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in
@@ -1145,7 +1145,7 @@ let default_morphism sign m =
     build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
   in
   let morph =
-    mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sign; m |])
+    mkApp (Lazy.force morphism_type, [| t; sign; m |])
   in
   let mor = resolve_one_typeclass env morph in
     mor, respect_projection mor morph
@@ -1156,7 +1156,7 @@ VERNAC COMMAND EXTEND AddSetoid1
 	let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
 	let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
 	let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
-	let instance = declare_instance a aeq n "Equivalence"
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	    anew_instance instance
 	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
@@ -1256,10 +1256,10 @@ let unification_rewrite l2r c1 c2 cl rel but gl =
 let get_hyp gl c clause l2r = 
   match kind_of_term (pf_type_of gl c) with
       Prod _ -> 
-	let hi = decompose_setoid_eqhyp gl c l2r in
+	let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
 	let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
 	  unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl
-    | _ -> decompose_setoid_eqhyp gl c l2r
+    | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r
 	
 let general_s_rewrite l2r c ~new_goals gl =
   let meta = Evarutil.new_meta() in
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5543f615d8..dd9cfbca5e 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -35,16 +35,16 @@ Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_refl : reflexive equiv.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_sym : symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_trans : transitive equiv.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 11c60a3aaf..2795e42188 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -22,10 +22,10 @@ Require Export Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
 Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 4fbbe2a408..c752cae869 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -46,7 +46,7 @@ Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity,
    The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
    for usual morphisms. *)
 
-Class Morphism A (R : relation A) (m : A) :=
+Class Morphism A (R : relation A) (m : A) : Prop :=
   respect : R m m.
 
 (** Here we build an equivalence instance for functions which relates respectful ones only. *)
@@ -54,7 +54,6 @@ Class Morphism A (R : relation A) (m : A) :=
 Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
   { morph : A -> B | respectful R R' morph morph }.
 
-
 Ltac obligations_tactic ::= program_simpl.
 
 Program Instance [ Equivalence A R, Equivalence B R' ] => 
@@ -63,21 +62,21 @@ Program Instance [ Equivalence A R, Equivalence B R' ] =>
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     destruct x ; simpl.
     apply r ; auto.
   Qed.
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     symmetry ; apply H.
     symmetry ; auto.
   Qed.
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     transitivity (proj1_sig y y0).
     apply H ; auto.
     apply H0. reflexivity.
@@ -116,51 +115,32 @@ Typeclasses unfold relation.
    them up to [impl] in each way. Very important instances as we need [impl]
    morphisms at the top level when we rewrite. *)
 
-Class SubRelation A (R S : relation A) :=
+Class SubRelation A (R S : relation A) : Prop :=
   subrelation :> Morphism (S ==> R) id.
 
 Instance iff_impl_subrelation : SubRelation Prop impl iff.
-Proof.
-  constructor ; red ; intros.
-  tauto.
-Qed.
+Proof. reduce. tauto. Qed.
 
 Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff.
 Proof.
-  constructor ; red ; intros.
-  tauto.
+  reduce. tauto.
 Qed.
 
-Instance [ SubRelation A R₁ R₂ ] =>
+Instance [ sub : SubRelation A R₁ R₂ ] =>
   morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂).
 Proof.
-  constructor ; repeat red. intros x y H x₁ y₁ H₁.
-  destruct subrelation.
-  red in respect0, H ; unfold id in *.
-  apply respect0.
-  apply H.
-  apply H₁.
+  reduce. apply* sub. apply H. assumption.
 Qed.
 
-Instance [ SubRelation A R₂ R₁ ] =>
+Instance [ sub : SubRelation A R₂ R₁ ] =>
   morphisms_subrelation_left : SubRelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
 Proof.
-  constructor ; repeat red ; intros x y H x₁ y₁ H₁.
-  destruct subrelation.
-  red in respect0, H ; unfold id in *.
-  apply H.
-  apply respect0.
-  apply H₁.
+  reduce. apply* H.  apply* sub. assumption.
 Qed.
 
 Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m.
 Proof.
-  intros.
-  destruct subrelation.
-  red in respect0 ; intros.
-  constructor.
-  unfold id in * ; apply respect0.
-  apply respect.
+  intros. apply* H. apply H0.
 Qed.
 
 Inductive done : nat -> Type :=
@@ -183,7 +163,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (* Typeclasses eauto := debug. *)
 
-Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ ! symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m.
 
   Next Obligation.
   Proof.
@@ -192,12 +172,12 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => 
   complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
-    unfold complement ; intros.
+    unfold complement.
     pose (respect).
     pose (r x y H).
     pose (r0 x0 y0 H0).
@@ -211,7 +191,6 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
 
   Next Obligation.
   Proof.
-    unfold inverse ; unfold flip.
     apply respect ; auto.
   Qed.
 
@@ -226,7 +205,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
 (** Every transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
-Program Instance [ ! Transitive A (R : relation A) ] => 
+Program Instance [ ! transitive A (R : relation A) ] => 
   trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
@@ -237,19 +216,15 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Dually... *)
 
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ ! transitive A (R : relation A) ] =>
   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
   
   Next Obligation.
   Proof with auto.
-    intros.
-    destruct (trans_contra_co_morphism (R:=inverse R)).
-    revert respect0.
-    unfold respectful, inverse, flip, impl in * ; intros.
-    eapply respect0 ; eauto.
+    apply* trans_contra_co_morphism ; eauto. eauto.
   Qed.
 
-(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *)
+(* Program Instance [ transitive A (R : relation A), symmetric A R ] => *)
 (*   trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *)
 
 (*   Next Obligation. *)
@@ -263,7 +238,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ ! transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -271,7 +246,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ ! transitive A R ] (x : A) =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -279,22 +254,20 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
-    symmetry...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
-    symmetry...
   Qed.
 
 Program Instance [ Equivalence A R ] (x : A) =>
@@ -311,7 +284,7 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** With symmetric relations, variance is no issue ! *)
 
 (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
-(*   [ Morphism _ (R ==> R') m ] [ Symmetric A R ] =>  *)
+(*   [ Morphism _ (R ==> R') m ] [ symmetric A R ] =>  *)
 (*   sym_contra_morphism : Morphism (R --> R') m. *)
 
 (*   Next Obligation. *)
@@ -323,48 +296,39 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** [R] is reflexive, hence we can build the needed proof. *)
 
 Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+  [ Morphism (R ==> R') m ] [ reflexive R ] (x : A) =>
   reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
-  Next Obligation.
-  Proof with auto.
-    intros.
-    apply (respect (m:=m))...
-    reflexivity.
-  Qed.
-
 (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ ! transitive A R ] => 
   trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
-    subst x0...
   Qed.
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ ! transitive A R ] => 
   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
   Proof with auto.
     transitivity x...
-    subst x0...
   Qed.
 
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ ! Transitive A R, Symmetric R ] => 
+Program Instance [ ! transitive A R, symmetric R ] => 
   trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    transitivity x0... transitivity x...
   
-    transitivity y... transitivity y0... symmetry...
+    transitivity y... transitivity y0... 
   Qed.
 
 Program Instance [ Equivalence A R ] => 
@@ -443,12 +407,12 @@ Program Instance or_iff_morphism :
 (*   red ; intros. subst ; split; trivial. *)
 (* Qed. *)
 
-Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
+Instance (A B : Type) [ ! reflexive B R ] (m : A -> B) =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
-Instance (A B : Type) [ ! Reflexive B R' ] => 
-  Reflexive (@Logic.eq A ==> R').
+Instance (A B : Type) [ ! reflexive B R' ] => 
+  reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
 (** [respectful] is a morphism for relation equivalence. *)
@@ -481,12 +445,13 @@ Proof.
   split ; intros ; intuition.
 Qed.
 
-Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) :=
+Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop :=
   normalizes : R m m'.
 
 Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
   Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof.
+  reduce.
   symmetry ; apply inverse_respectful.
 Qed.
 
@@ -494,6 +459,7 @@ Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B)
   [ Normalizes relation_equivalence R' (inverse R'') ] =>
   Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
 Proof.
+  red.
   pose normalizes.
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
@@ -504,19 +470,13 @@ Program Instance (A : Type) (R : relation A)
   [ Morphism R m ] => morphism_inverse_morphism :
   Morphism (inverse R) m | 2.
 
-  Next Obligation.
-  Proof.
-    apply respect.
-  Qed.
-
 (** Bootstrap !!! *)
 
 Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
 Proof.
-  simpl_relation.
-  subst.
+  simpl_relation. 
   unfold relation_equivalence in H.
-  split ; constructor ; intros.
+  split ; red ; intros.
   setoid_rewrite <- H.
   apply respect.
   setoid_rewrite H.
@@ -527,7 +487,7 @@ Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
   [ Normalizes relation_equivalence R R' ]
   [ Morphism R' m ] : Morphism R m.
 Proof.
-  intros. 
+  intros.
   pose respect.
   assert(n:=normalizes).
   setoid_rewrite n.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b053b27f24..53079674f7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- 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 *)
@@ -50,133 +50,139 @@ Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
-Class Reflexive A (R : relation A) :=
-  reflexive : forall x, R x x.
+Class reflexive A (R : relation A) :=
+  reflexivity : forall x, R x x.
 
-Class Irreflexive A (R : relation A) := 
-  irreflexive : forall x, R x x -> False.
+Class irreflexive A (R : relation A) := 
+  irreflexivity : forall x, R x x -> False.
 
-Class Symmetric A (R : relation A) := 
-  symmetric : forall x y, R x y -> R y x.
+Class symmetric A (R : relation A) := 
+  symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric A (R : relation A) := 
-  asymmetric : forall x y, R x y -> R y x -> False.
+Class asymmetric A (R : relation A) := 
+  asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive A (R : relation A) := 
-  transitive : forall x y z, R x y -> R y z -> R x z.
+Class transitive A (R : relation A) := 
+  transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments Reflexive [A].
-Implicit Arguments Irreflexive [A].
-Implicit Arguments Symmetric [A].
-Implicit Arguments Asymmetric [A].
-Implicit Arguments Transitive [A].
+Implicit Arguments reflexive [A].
+Implicit Arguments irreflexive [A].
+Implicit Arguments symmetric [A].
+Implicit Arguments asymmetric [A].
+Implicit Arguments transitive [A].
 
-Hint Resolve @irreflexive : ord.
+Hint Resolve @irreflexivity : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) :=
-  reflexive := reflexive (R:=R).
+Program Instance [ ! reflexive A R ] => flip_reflexive : reflexive (flip R) :=
+  reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) :=
-  irreflexive := irreflexive (R:=R).
+Program Instance [ ! irreflexive A R ] => flip_irreflexive : irreflexive (flip R) :=
+  irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R).
+Program Instance [ ! symmetric A R ] => flip_symmetric : symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R).
+Program Instance [ ! asymmetric A R ] => flip_asymmetric : asymmetric (flip R).
   
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric.
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R).
+Program Instance [ ! transitive A R ] => flip_transitive : transitive (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; clapply transitive.
+  Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) :=
-  reflexive := reflexive (R:=R).
+Program Instance [ ! reflexive A (R : relation A) ] => inverse_reflexive : reflexive (inverse R) :=
+  reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) :=
-  irreflexive := irreflexive (R:=R).
+Program Instance [ ! irreflexive A (R : relation A) ] => inverse_irreflexive : irreflexive (inverse R) :=
+  irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R).
+Program Instance [ ! symmetric A (R : relation A) ] => inverse_symmetric : symmetric (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R).
+Program Instance [ ! asymmetric A (R : relation A) ] => inverse_asymmetric : asymmetric (inverse R).
   
-  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric.
+  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R).
+Program Instance [ ! transitive A (R : relation A) ] => inverse_transitive : transitive (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ ! Reflexive A (R : relation A) ] => 
-  reflexive_complement_irreflexive : Irreflexive (complement R).
+Program Instance [ ! reflexive A (R : relation A) ] => 
+  reflexive_complement_irreflexive : irreflexive (complement R).
 
-  Next Obligation. 
-  Proof. 
-    apply H.
-    apply reflexive.
-  Qed.
-
-Program Instance [ ! Irreflexive A (R : relation A) ] => 
-  irreflexive_complement_reflexive : Reflexive (complement R).
+Program Instance [ ! irreflexive A (R : relation A) ] => 
+  irreflexive_complement_reflexive : reflexive (complement R).
 
   Next Obligation. 
   Proof. 
     red. intros H.
-    apply (irreflexive H).
+    apply (irreflexivity H).
   Qed.
 
-Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R).
+Program Instance [ ! symmetric A (R : relation A) ] => complement_symmetric : symmetric (complement R).
 
   Next Obligation.
   Proof.
     red ; intros H'.
-    apply (H (symmetric H')).
+    apply (H (symmetry H')).
   Qed.
 
 (** * Standard instances. *)
 
+Ltac reduce_goal :=
+  match goal with
+    | [ |- _ <-> _ ] => fail 1
+    | _ => red ; intros ; try reduce_goal
+  end.
+
+Ltac reduce := reduce_goal.
+
+Tactic Notation "apply" "*" constr(t) := 
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
 Ltac simpl_relation :=
-  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
-    repeat (red ; intros) ; try ( solve [ intuition ]).
+  unfold inverse, flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ intuition ]).
 
 Ltac obligations_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
-Program Instance impl_refl : Reflexive impl.
-Program Instance impl_trans : Transitive impl.
+Program Instance impl_refl : reflexive impl.
+Program Instance impl_trans : transitive impl.
 
 (** Logical equivalence. *)
 
-Program Instance iff_refl : Reflexive iff.
-Program Instance iff_sym : Symmetric iff.
-Program Instance iff_trans : Transitive iff.
+Program Instance iff_refl : reflexive iff.
+Program Instance iff_sym : symmetric iff.
+Program Instance iff_trans : transitive iff.
 
 (** Leibniz equality. *)
 
-Program Instance eq_refl : Reflexive (@eq A).
-Program Instance eq_sym : Symmetric (@eq A).
-Program Instance eq_trans : Transitive (@eq A).
+Program Instance eq_refl : reflexive (@eq A).
+Program Instance eq_sym : symmetric (@eq A).
+Program Instance eq_trans : transitive (@eq A).
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
 (** A [PreOrder] is both reflexive and transitive. *)
 
 Class PreOrder A (R : relation A) :=
-  preorder_refl :> Reflexive R ;
-  preorder_trans :> Transitive R.
+  preorder_refl :> reflexive R ;
+  preorder_trans :> transitive R.
 
 (** A partial equivalence relation is symmetric and transitive. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
-  per_sym :> Symmetric pequiv ;
-  per_trans :> Transitive pequiv.
+  per_sym :> symmetric pequiv ;
+  per_trans :> transitive pequiv.
 
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
@@ -187,33 +193,28 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 
   Next Obligation.
   Proof with auto.
-    constructor ; intros...
     assert(R x0 x0). 
-    clapply transitive. clapply symmetric.
-    clapply transitive. 
+    transitivity y0... symmetry...
+    transitivity (y x0)...
   Qed.
 
 (** The [Equivalence] typeclass. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) :=
-  equiv_refl :> Reflexive equiv ;
-  equiv_sym :> Symmetric equiv ;
-  equiv_trans :> Transitive equiv.
+  equiv_refl :> reflexive equiv ;
+  equiv_sym :> symmetric equiv ;
+  equiv_trans :> transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
-  antisymmetric : forall x y, R x y -> R y x -> eqA x y.
-
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
-  flip_antisymmetric : Antisymmetric eq (flip R).
-
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
+Class [ Equivalence A eqA ] => antisymmetric (R : relation A) := 
+  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
-  inverse_antisymmetric : Antisymmetric eq (inverse R).
+Program Instance [ eq : Equivalence A eqA, antisymmetric eq R ] => 
+  flip_antisymmetric : antisymmetric eq (flip R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
+Program Instance [ eq : Equivalence A eqA, antisymmetric eq (R : relation A) ] => 
+  inverse_antisymmetric : antisymmetric eq (inverse R).
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
@@ -240,18 +241,6 @@ Program Instance relation_equivalence_equivalence :
 
   Next Obligation.
   Proof.
-    constructor ; red ; intros.
-    apply reflexive.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; red ; intros.
-    apply symmetric ; apply H.
-  Qed.
-  
-  Next Obligation.
-  Proof.
-    constructor ; red ; intros.
-    apply transitive with (y x0 y0) ; [ apply H | apply H0 ].
+    unfold relation_equivalence in *.
+    apply transitivity with (y x0 y0) ; [ apply H | apply H0 ].
   Qed.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5cf33542c3..d2ee4f443c 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -40,13 +40,13 @@ Typeclasses unfold @equiv.
 
 (** Shortcuts to make proof search easier. *)
 
-Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Definition setoid_refl [ sa : Setoid A ] : reflexive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Definition setoid_sym [ sa : Setoid A ] : symmetric equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Definition setoid_trans [ sa : Setoid A ] : transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
 Existing Instance setoid_refl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 9f6dfab423..ee8c530fa2 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -74,7 +74,7 @@ Ltac red_subst_eq_morphism concl :=
 
 Ltac destruct_morphism :=
   match goal with
-    | [ |- @Morphism ?A ?R ?m ] => constructor
+    | [ |- @Morphism ?A ?R ?m ] => red
   end.
 
 Ltac reverse_arrows x :=
@@ -91,4 +91,3 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
-
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index b0c8ee008c..0c19176f82 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -431,7 +431,7 @@ Add Relation t Subset
 
 Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
 Proof.
-  do 2 red ; intros. unfold Subset, impl; intros; eauto with set.
+  simpl_relation. eauto with set.
 Qed.
 
 Add Morphism Empty with signature Subset --> impl as Empty_s_m.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3896f02dda..cff8bce1e5 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -129,26 +129,21 @@ let declare_implicit_proj c proj imps sub =
     Impargs.declare_manual_implicits true (ConstRef proj) true expls
       
 let declare_implicits impls subs cl =
-  let projs = Recordops.lookup_projections cl.cl_impl in
-    Util.list_iter3
-      (fun c imps sub -> 
-	match c with 
-	  | None -> assert(false)
-	  | Some p -> declare_implicit_proj cl p imps sub)
-      projs impls subs;
-    let len = List.length cl.cl_context in
-    let indimps = 
-      list_fold_left_i 
-	(fun i acc (is, (na, b, t)) -> 
-	  if len - i <= cl.cl_params then acc
-	  else 
-	    match is with
-		None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc
-	      | _ -> acc)
-	1 [] (List.rev cl.cl_context)
-    in
-      Impargs.declare_manual_implicits true (IndRef cl.cl_impl) false indimps
-
+  Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
+    cl.cl_projs impls subs;
+  let len = List.length cl.cl_context in
+  let indimps = 
+    list_fold_left_i 
+      (fun i acc (is, (na, b, t)) -> 
+	if len - i <= cl.cl_params then acc
+	else 
+	  match is with
+	      None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc
+	    | _ -> acc)
+      1 [] (List.rev cl.cl_context)
+  in
+    Impargs.declare_manual_implicits true cl.cl_impl false indimps
+      
 let rel_of_named_context subst l = 
   List.fold_right
     (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
@@ -277,26 +272,54 @@ let new_class id par ar sup props =
   let ctx_props = Evarutil.nf_named_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 kn = 
-    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
+  let impl, projs = 
     let params, subst = rel_of_named_context [] ctx_params in
     let fields, _ = rel_of_named_context subst ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
-      declare_structure env0 (snd id) idb params arity fields
+      match fields with
+	  [(Name proj_name, _, field)] ->
+	    let class_type = it_mkProd_or_LetIn arity params in
+	    let class_body = it_mkLambda_or_LetIn field params in
+	    let class_entry = 
+	      { const_entry_body = class_body;
+		const_entry_type = Some 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
+	      ConstRef cst, [proj_cst]
+	| _ ->
+	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
+	    let kn = declare_structure env0 (snd id) idb params arity fields in
+	      IndRef kn, (List.map Option.get (Recordops.lookup_projections kn))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
       match Typeclasses.class_of_constr t with
-	| Some cl -> (Some (cl.cl_name, List.exists (fun (_, n) -> n = Name na) supnames), d)
+	| Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d)
 	| None -> (None, d))
       ctx_params
   in
   let k =
-    { cl_name = snd id;
+    { cl_impl = impl;
       cl_params = List.length par;
       cl_context = ctx_context;
       cl_props = ctx_props;
-      cl_impl = kn }
+      cl_projs = projs }
   in
     declare_implicits (List.rev prop_impls) subs k;
     add_class k
@@ -324,15 +347,7 @@ let subst_named inst subst ctx =
       (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
       ctx' ([], 0)
   in ctx'
-
-let destClass c = 
-  match kind_of_term c with
-      App (c, args) -> 
-	(match kind_of_term c with
-	  | Ind ind -> (try class_of_inductive ind, args with _ -> assert false)
-	  | _ -> assert false)
-    | _ -> assert false
-
+(*
 let infer_super_instances env params params_ctx super =
   let super = subst_named params params_ctx super in
     List.fold_right 
@@ -346,7 +361,7 @@ let infer_super_instances env params params_ctx super =
 	in
 	let d = (na, Some inst, t) in
 	  inst :: sups, na :: ids, d :: supctx)
-      super ([], [], [])
+      super ([], [], [])*)
       
 (* let evars_of_context ctx id n env = *)
 (*   List.fold_right (fun (na, _, t) (n, env, nc) ->  *)
@@ -374,6 +389,14 @@ let destClassApp cl =
 
 let refine_ref = ref (fun _ -> assert(false))
 
+let id_of_class cl =
+  match cl.cl_impl with
+    | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
+    | IndRef (kn,i) -> 
+	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
+	  mip.(0).Declarations.mind_typename
+    | _ -> assert false
+	
 open Pp
 
 let ($$) g f = fun x -> g (f x)
@@ -386,11 +409,8 @@ let new_instance ctx (instid, bk, cl) props pri hook =
   let tclass = 
     match bk with
       | Explicit ->
-	  let id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = 
-	    try class_info (snd id)
-	    with Not_found -> unbound_class env id
-	  in
+	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
+	  let k = class_info (global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
 	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
 	    if needlen <> applen then 
@@ -407,7 +427,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
 		      in t, avoid
 		  | None -> failwith ("new instance: under-applied typeclass"))
 	      par (List.rev k.cl_context)
-	    in Topconstr.CAppExpl (Util.dummy_loc, (None, Ident id), pars)
+	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
       | Implicit -> cl
   in
@@ -421,13 +441,8 @@ let new_instance ctx (instid, bk, cl) props pri hook =
     let c = Command.generalize_constr_expr tclass ctx in
     let _imps, c' = interp_type_evars isevars env c in
     let ctx, c = decompose_named_assum c' in
-      (match kind_of_term c with 
-	  App (c, args) -> 
-	    let cl = Option.get (class_of_constr c) in
-	      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
-	| _ -> 
-	    let cl = Option.get (class_of_constr c) in
-	      cl, ctx, [])
+    let cl, args = Typeclasses.dest_class_app c in
+      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -437,7 +452,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
 	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
 	    id
       | Anonymous -> 
-	  let i = Nameops.add_suffix k.cl_name "_instance_0" in
+	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
   let env' = push_named_context ctx' env in
@@ -465,18 +480,17 @@ let new_instance ctx (instid, bk, cl) props pri hook =
 	  ([], props) k.cl_props
       in
 	if rest <> [] then 
-	  unbound_method env' k.cl_name (fst (List.hd rest))
+	  unbound_method env' k.cl_impl (fst (List.hd rest))
 	else
 	  type_ctx_instance isevars env' k.cl_props props substctx
   in
-  let app = 
-    applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
-  in 
+  let inst_constr, ty_constr = instance_constructor k in
+  let app = inst_constr (List.rev_map snd subst) in 
   let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
   isevars := Evarutil.nf_evar_defs !isevars;
   let term = Evarutil.nf_isevar !isevars term in
   let termtype = 
-    let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
+    let app = applistc ty_constr (List.rev_map snd substctx) in
     let t = it_mkNamedProd_or_LetIn app ctx' in
       Evarutil.nf_isevar !isevars t
   in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 248ed8c956..6671eed72d 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -29,10 +29,10 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
 val binders_of_lidents : identifier located list -> local_binder list
 
 val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> bool -> unit
-
+(*
 val infer_super_instances : env -> constr list ->
   named_context -> named_context -> types list * identifier list * named_context
-
+*)
 val new_class : identifier located ->
   local_binder list ->
   Vernacexpr.sort_expr located ->
@@ -46,6 +46,9 @@ val new_instance :
   int option ->
   (constant -> unit) ->
   identifier
+
+(* For generation on names based on classes only *)
+val id_of_class : typeclass -> identifier
     
 val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
 
@@ -76,3 +79,4 @@ val push_named_context : named_context -> env -> env
 val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
+
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4d1b608e6b..70441e50d6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -471,12 +471,12 @@ let explain_pretype_error env err =
       
 (* Typeclass errors *)
 
-let explain_unbound_class env (_,id) =
-  str "Unbound class name " ++ Nameops.pr_id id
+let explain_not_a_class env c =
+  pr_constr_env env c ++ str" is not a declared type class"
 
 let explain_unbound_method env cid id =
   str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ 
-    Nameops.pr_id cid
+    pr_global cid
 
 let pr_constr_exprs exprs = 
   hv 0 (List.fold_right 
@@ -495,7 +495,7 @@ let explain_mismatched_contexts env c i j =
 
 let explain_typeclass_error env err = 
   match err with
-    | UnboundClass id -> explain_unbound_class env id
+    | NotAClass c -> explain_not_a_class env c
     | UnboundMethod (cid, id) -> explain_unbound_method env cid id
     | NoInstance (id, l) -> explain_no_instance env id l
     | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 45a0f834ba..4e29013199 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -227,6 +227,9 @@ let dump_universes s =
   with
       e -> close_out output; raise e
 
+let print_instances c =
+  ppnl (Prettyp.print_instances (global c))
+
 (*********************)
 (* "Locate" commands *)
 
@@ -974,7 +977,7 @@ let vernac_print = function
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
   | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
-  | PrintInstances c -> ppnl (Prettyp.print_instances c)
+  | PrintInstances c -> print_instances c 
   | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->