Code cleanup in typeclasses, remove dead and duplicated code.

Change from named_context to rel_context for class params and fields.


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

13 files changed, 119 insertions, 572 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 67b3adede..aa16bd4bb 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -73,26 +73,17 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
+      let t' = substl subst t in
       let c = interp_casted_constr_evars isevars env ce t' in
       let d = na, Some c, t' in
-	(na, c) :: subst, d :: instctx)
+	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
-
 let type_class_instance_params isevars env id n ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
       let t' = replace_vars subst t in
-      let c = 
-(* 	if ce = superclass_ce then *)
-	(* 	  (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
-	(* 	     in instance search. *\) *)
-	(* 	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
-	(* 	else *)
-	interp_casted_constr_evars isevars env ce t' 
-      in
+      let c = interp_casted_constr_evars isevars env ce t' in
       let d = na, Some c, t' in
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
@@ -140,9 +131,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
-    let ctx, c = Classes.decompose_named_assum c' in
+    let ctx, c = Sign.decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -155,11 +146,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	  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
+  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 = Typeclasses.nf_substitution sigma subst in
+  let substctx = List.map (Evarutil.nf_evar sigma) subst in
   let subst, _propsctx = 
     let props = 
       List.map (fun (x, l, d) -> 
@@ -172,8 +163,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	List.fold_left
 	  (fun (props, rest) (id,_,_) -> 
 	    try 
-	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+	      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
 		Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		c :: props, rest'
 	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -184,20 +175,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	else
 	  type_ctx_instance isevars env' k.cl_props props substctx
   in
-  let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) 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_mkNamedLambda_or_LetIn inst_constr ctx')
-    and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') 
+    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 imps =  *)
-(*     Util.list_map_i  *)
-(*       (fun i binder -> *)
-(* 	match binder with *)
-(* 	ExplByPos (i, Some na), (true, true)) *)
-(*       1 ctx *)
-(*   in *)
       let hook gr = 
 	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 	let inst = Typeclasses.new_instance k pri global cst in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 99231f585..1cb03385b 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -26,11 +26,11 @@ open Classes
 
 val type_ctx_instance :     Evd.evar_defs ref ->
     Environ.env ->
-    (Names.identifier * 'a * Term.constr) list ->
+    ('a * Term.constr option * Term.constr) list ->
     Topconstr.constr_expr list ->
-    (Names.identifier * Term.constr) list ->
-    (Names.identifier * Term.constr) list *
-    (Names.identifier * Term.constr option * Term.constr) list
+    Term.constr list ->
+    Term.constr list *
+    ('a * Term.constr option * Term.constr) list
 
 val new_instance : 
   ?global:bool ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ac4639b43..1ddcac276 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1275,23 +1275,6 @@ let intern_ltac isarity ltacvars sigma env c =
 
 type manual_implicits = (explicitation * (bool * bool)) list
 
-let implicits_of_rawterm l = 
-  let rec aux i c = 
-    match c with
-	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
-	  let rest = aux (succ i) b in
-	    if bk = Implicit then
-	      let name =
-		match na with
-		    Name id -> Some id
-		  | Anonymous -> None
-	      in
-		(ExplByPos (i, name), (true, true)) :: rest
-	    else rest
-      | RLetIn (loc, na, t, b) -> aux i b
-      | _ -> []
-  in aux 1 l
-
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
@@ -1321,11 +1304,11 @@ let interp_constr_evars_gen_impls ?evdref
   match evdref with 
     | None -> 
 	let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_gen kind Evd.empty env c, imps
     | Some evdref ->
 	let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_tcc_evars evdref env kind c, imps
 
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bb5a4412c..bef2573e5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -29,7 +29,6 @@ open Pp
 let ids_of_list l = 
   List.fold_right Idset.add l Idset.empty
 
-
 let locate_reference qid =
   match Nametab.extended_locate qid with
     | TrueGlobal ref -> true
@@ -88,44 +87,17 @@ let rec make_fresh ids env x =
 let freevars_of_ids env ids = 
   List.filter (is_freevar env (Global.env())) ids
 
-let compute_constrs_freevars env constrs =
-  let ids = 
-    List.rev (List.fold_left 
-		 (fun acc x -> free_vars_of_constr_expr x acc) 
-		 [] constrs)
-  in freevars_of_ids env ids
-
-(* let compute_context_freevars env ctx = *)
-(*   let ids = *)
-(*     List.rev *)
-(*       (List.fold_left *)
-(* 	  (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *)
-(* 	  [] constrs) *)
-(*   in freevars_of_ids ids *)
-
-let compute_constrs_freevars_binders env constrs =
-  let elts = compute_constrs_freevars env constrs in
-    List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
-
 let binder_list_of_ids ids =
   List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-(*   let rec name_rec id = *)
-(*     if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in  *)
-(*   name_rec id  *)
-
-let ids_of_named_context_avoiding avoid l =
-  List.fold_left (fun (ids, avoid) id -> 
-    let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid) 
-    ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid fn applied needed =
   let named, applied = 
     List.partition 
       (function
 	  (t, Some (loc, ExplByName id)) -> 
-	    if not (List.exists (fun (_, (id', _, _)) -> id = id') needed) then
+	    if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then
 	      user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
 	    true
 	| _ -> false) applied
@@ -138,13 +110,13 @@ let combine_params avoid fn applied needed =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (id, _, _)) :: need when List.mem_assoc id named ->
+      | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named ->
 	  aux (List.assoc id named :: ids) avoid app need
 	    
-      | (x, None) :: app, (None, (id, _, _)) :: need ->
+      | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 	    
-      | _, (Some cl, (id, _, _) as d) :: need -> 
+      | _, (Some cl, (Name id, _, _) as d) :: need -> 
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -155,12 +127,14 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
+
+      | _, _ -> raise (Invalid_argument "combine_params")
   in aux [] avoid applied needed
 
 let combine_params_freevar avoid applied needed =
   combine_params avoid
     (fun avoid (_, (id, _, _)) -> 
-      let id' = next_ident_away_from id avoid in
+      let id' = next_ident_away_from (Nameops.out_name id) avoid in
 	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
     applied needed
 
@@ -201,19 +175,6 @@ let full_class_binders env l =
 	| Explicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'
-      
-let constr_expr_of_constraint (kind, id) l =
-  match kind with
-    | Implicit -> CAppExpl (fst id, (None, Ident id), l)
-    | Explicit -> CApp (fst id, (None, CRef (Ident id)),
-		       List.map (fun x -> x, None) l)
-
-(*    | CApp of loc * (proj_flag * constr_expr) *  *)
-(*         (constr_expr * explicitation located option) list *)
-
-
-let constrs_of_context l =
-  List.map (fun (_, id, l) -> constr_expr_of_constraint id l) l
 
 let compute_context_freevars env ctx =
   let bound, ids = 
@@ -232,41 +193,12 @@ let resolve_class_binders env l =
   in
     fv_ctx, ctx
 
-let generalize_class_binders env l = 
-  let fv_ctx, cstrs = resolve_class_binders env l in
-    List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx,
-  List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c)) 
-    cstrs
-
 let generalize_class_binders_raw env l = 
   let env = Idset.union env (Termops.vars_of_env (Global.env())) in
   let fv_ctx, cstrs = resolve_class_binders env l in
     List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
   List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
-
-let ctx_of_class_binders env l = 
-  let (x, y) = generalize_class_binders env l in x @ y
 	
-let implicits_of_binders l = 
-  let rec aux i l = 
-    match l with 
-	[] -> []
-      | hd :: tl -> 
-	  let res, reslen = 
-	    match hd with
-		LocalRawAssum (nal, Default Implicit, t) -> 
-		  list_map_i (fun i (_,id) ->
-		    let name =
-		      match id with
-			  Name id -> Some id
-			| Anonymous -> None
-		    in ExplByPos (i, name), (true, true))
-		    i nal, List.length nal
-	      | LocalRawAssum (nal, _, _) -> [], List.length nal
-	      | LocalRawDef _ -> [], 1
-	  in res @ (aux (i + reslen) tl)
-  in aux 1 l
-  
 let implicits_of_rawterm l = 
   let rec aux i c = 
     match c with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 018c471d4..bd061a1ed 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -39,8 +39,6 @@ val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
-val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
-val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
 val resolve_class_binders : Idset.t -> typeclass_context -> 
   (identifier located * constr_expr) list * typeclass_context
 
@@ -49,20 +47,12 @@ val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
 val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
   (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
 
-val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list
-
-val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list
-
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  ((global_reference * bool) option * Term.named_declaration) list ->
+  ((global_reference * bool) option * Term.rel_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
-
-val ids_of_named_context_avoiding :     Names.Idset.t ->
-    Sign.named_context -> Names.Idset.elt list * Names.Idset.t
-
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1b3c2baea..e75be25f3 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -35,12 +35,12 @@ type typeclass = {
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : ((global_reference * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * rel_declaration) list; 
 
   cl_params: int;
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : named_context;
+  cl_props : rel_context;
   
   (* The method implementaions as projections. *)
   cl_projs : (identifier * constant) list;
@@ -176,8 +176,14 @@ let subst (_,subst,(cl,m,inst)) =
     (classes, m, instances)
 
 let discharge (_,(cl,m,inst)) =
-  let discharge_named (cl, r) =
-    Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r
+  let discharge_context subst rel =
+    let ctx, _ =
+      List.fold_right
+	(fun (gr, (id, b, t)) (ctx, k) -> 
+	  let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in
+	    ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
+	rel ([], 0)
+    in ctx
   in
   let abs_context cl =
     match cl.cl_impl with
@@ -190,10 +196,11 @@ let discharge (_,(cl,m,inst)) =
     let cl' =
       if cl_impl' == cl.cl_impl then cl
       else
+	let ctx = abs_context cl in
 	{ cl with cl_impl = cl_impl';
 	  cl_context = 
-	    List.map (fun x -> None, x) (abs_context cl) @	
-	      (list_smartmap discharge_named cl.cl_context);
+	    List.map (fun (na,b,t) -> None, (Name na,b,t)) ctx @
+	      (discharge_context (List.map pi1 ctx) cl.cl_context);
 	  cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
     in Gmap.add cl_impl' cl' acc
   in
@@ -280,46 +287,6 @@ let add_instance i =
 let instances r = 
   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)
-
-let resolve_typeclass env ev evi (evd, defined as acc) =
-  try
-    assert(evi.evar_body = Evar_empty);
-    !solve_instanciation_problem env evd ev evi
-  with Exit -> acc
-
-let resolve_one_typeclass env types =
-  try
-    let evi = Evd.make_evar (Environ.named_context_val env) types in
-    let ev = 1 in
-    let evm = Evd.add Evd.empty ev evi in
-    let evd = Evd.create_evar_defs evm in
-    let evd', b = !solve_instanciation_problem env evd ev evi in
-      if b then 
-	let evm' = Evd.evars_of evd' in
-	  match Evd.evar_body (Evd.find evm' ev) with
-	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
-      else raise Not_found
-  with Exit -> raise Not_found
-
-let resolve_one_typeclass_evd env evd types =
-  try
-    let ev = Evarutil.e_new_evar evd env types in
-    let (ev,_) = destEvar ev in
-    let evd', b =
-	!solve_instanciation_problem env !evd ev (Evd.find (Evd.evars_of !evd) ev)
-    in
-      evd := evd';
-      if b then 
-	let evm' = Evd.evars_of evd' in
-	  match Evd.evar_body (Evd.find evm' ev) with
-	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> Evarutil.nf_evar evm' c
-      else raise Not_found
-  with Exit -> raise Not_found
-
 let method_typeclass ref = 
   match ref with 
     | ConstRef c -> 
@@ -348,51 +315,6 @@ let is_implicit_arg k =
       ImplicitArg (ref, (n, id)) -> true
     | InternalHole -> true
     | _ -> false
-
-let destClassApp c = 
-  match kind_of_term c with
-    | App (ki, args) when isInd ki -> 
-	Some (destInd ki, args)
-    | _ when isInd c -> Some (destInd c, [||])
-    | _ -> None
-
-let is_independent evm ev = 
-  Evd.fold (fun ev' evi indep -> indep && 
-    (ev = ev' || 
-	evi.evar_body <> Evar_empty ||
-	not (Termops.occur_evar ev evi.evar_concl)))
-    evm true
-    
-
-(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
-(*   with _ -> *)
-(*   let evm = Evd.evars_of evd in *)
-(*   let tc_evars =  *)
-(*     let f ev evi acc = *)
-(*       let (l, k) = Evd.evar_source ev evd in *)
-(* 	if not check || is_implicit_arg k then *)
-(* 	  match destClassApp evi.evar_concl with *)
-(* 	    | Some (i, args) when is_class i ->  *)
-(* 		Evd.add acc ev evi *)
-(* 	    | _ -> acc *)
-(* 	else acc *)
-(*     in Evd.fold f evm Evd.empty *)
-(*   in *)
-(*   let rec sat evars = *)
-(*     let evm = Evd.evars_of evars in *)
-(*     let (evars', progress) =  *)
-(*       Evd.fold  *)
-(* 	(fun ev evi acc ->  *)
-(* 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev))  *)
-(* 	    && evi.evar_body = Evar_empty then *)
-(* 	    resolve_typeclass env ev evi acc  *)
-(* 	  else acc) *)
-(* 	evm (evars, false)  *)
-(*     in *)
-(*       if not progress then evars' *)
-(*       else *)
-(* 	sat (Evarutil.nf_evar_defs evars') *)
-(*   in sat (Evarutil.nf_evar_defs evd) *)
   
 let class_of_constr c = 
   let extract_cl c =
@@ -438,20 +360,9 @@ let has_typeclasses evd =
 	&& is_resolvable evi))
     evd false
 
+let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
+
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
     !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
-
-type substitution = (identifier * constr) list
-
-let substitution_of_named_context isevars env id n subst l = 
-  List.fold_right
-    (fun (na, _, t) subst -> 
-      let t' = replace_vars subst t in
-      let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' in
-	(na, b) :: subst)
-    l subst
-
-let nf_substitution sigma subst = 
-  List.map (function (na, c) -> na, Reductionops.nf_evar sigma c) subst
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 412b99e57..09f6a7696 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -30,12 +30,12 @@ type typeclass = {
 
   (* 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 : ((global_reference * bool) option * named_declaration) list; 
+  cl_context : ((global_reference * bool) option * rel_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;
+  cl_props : rel_context;
 
   (* The methods implementations of the typeclass as projections. *)
   cl_projs : (identifier * constant) list;
@@ -43,33 +43,31 @@ type typeclass = {
 
 type instance
 
-val instance_impl : instance -> constant
-
-val new_instance : typeclass -> int option -> bool -> constant -> instance
-  
 val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list
+
 val add_class : typeclass -> unit
-val add_instance : instance -> unit
 
-val register_add_instance_hint : (constant -> int option -> unit) -> unit
-val add_instance_hint : constant -> int option -> unit
+val new_instance : typeclass -> int option -> bool -> constant -> instance
+val add_instance : instance -> unit
 
 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 *)
 
+val instance_impl : instance -> constant
+
+val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
 val is_method : constant -> bool
 
+val is_implicit_arg : hole_kind -> bool
+
 (* Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
-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 resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
+val instance_constructor : typeclass -> constr list -> constr * types
 
 (* Use evar_extra for marking resolvable evars. *)
 val bool_in : bool -> Dyn.t
@@ -81,25 +79,7 @@ val mark_unresolvables : evar_map -> evar_map
 
 val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
 
-val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
-val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
-
-type substitution = (identifier * constr) list
-
-val substitution_of_named_context : 
-  evar_defs ref -> env -> identifier -> int ->
-  substitution -> named_context -> substitution
-
-val nf_substitution : evar_map -> substitution -> substitution
-
-val is_implicit_arg : hole_kind -> bool
-
-(* 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 *)
+val register_add_instance_hint : (constant -> int option -> unit) -> unit
+val add_instance_hint : constant -> int option -> unit
 
+val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 090776018..ba3eae6fa 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -29,7 +29,7 @@ type typeclass_error =
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
-    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index df196ae4c..3f0723ad8 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -29,7 +29,7 @@ type typeclass_error =
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
-    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -41,4 +41,4 @@ val no_instance : env -> identifier located -> constr list -> 'a
 
 val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
 
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a
+val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index cca6ac0fc..84f9eb3ff 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -442,8 +442,8 @@ let rec add_directory recur add_file phys_dir log_dir =
   try
     while true do
       let f = readdir dirh in
-      (* we avoid . .. and all hidden files and subdirs (e.g. .svn) *)
-      if f.[0] <> '.' then
+      (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *)
+      if f.[0] <> '.' && f.[0] <> '_' then
         let phys_f = phys_dir//f in
 	match try (stat phys_f).st_kind with _ -> S_BLK with
 	  | S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f])
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0d24a6edd..30fee26a0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -61,11 +61,12 @@ let declare_instance glob idl =
   in declare_instance_cst glob con
 	  
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 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) -> 
@@ -87,33 +88,26 @@ let interp_typeclass_context_evars isevars env avoid l =
 	(push_named d env, i :: ids, d::params))
     (env, avoid, []) l
 
-let interp_constrs_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) t -> 
-      let t' = interp_binder_evars isevars env Anonymous t in
-      let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
-      let d = (id,None,t') in
-	(push_named d env, id :: ids, d::params))
-    (env, avoid, []) l
-
-let raw_assum_of_binders k = 
-  List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t))
-
-let raw_assum_of_constrs k = 
-  List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t))
-
-let raw_assum_of_anonymous_constrs k = 
-  List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t))
+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 decl_expr_of_binders = 
-  List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t))
-      
-let rec unfold n f acc = 
-  match n with 
-    | 0 -> f 0 acc
-    | n -> unfold (n - 1) f (f n acc)
+let mk_interning_data env na impls typ =
+  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
+  in (na, ([], 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 declare_implicit_proj c proj imps sub =
@@ -144,22 +138,12 @@ let declare_implicits impls subs cl =
 	if len - i <= cl.cl_params then acc
 	else 
 	  match is with
-	      None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc
+	      None | Some (_, false) -> (ExplByPos (i, Some (Nameops.out_name na)), (false, true)) :: acc
 	    | _ -> acc)
       1 [] (List.rev cl.cl_context)
   in
     Impargs.declare_manual_implicits false 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)
-    l ([], subst)
-
-let ids_of_rel_context subst l = 
-  List.fold_right
-    (fun (id, _, t) acc -> Nameops.out_name id :: acc)
-    l subst
-
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
@@ -168,7 +152,6 @@ let degenerate_decl (na,b,t) =
     | None -> (id, Entries.LocalAssum t)
     | Some b -> (id, Entries.LocalDef b)
 
-
 let declare_structure env id idbuild params arity fields =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
@@ -192,33 +175,6 @@ let declare_structure env id idbuild params arity fields =
     Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
     rsp
 
-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, ([], 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 = (i,None,t') in
-	(push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
-    (env, [], avoid, [], ([], [])) l    
-
-let interp_fields_rel_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    
-
 let name_typeclass_binder avoid = function
   | LocalRawAssum ([loc, Anonymous], bk, c) ->
       let name = 
@@ -237,33 +193,7 @@ let name_typeclass_binders avoid l =
 				   b' :: binders, avoid)
       ([], avoid) l
   in List.rev l', avoid
-
-let decompose_named_assum = 
-  let rec prodec_rec subst l c =
-    match kind_of_term c with
-      | Prod (Name na,t,c) -> 
-	let decl = (na,None,substl subst t) in
-	let subst' = mkVar na :: subst in
-	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
-      | LetIn (Name na, b, t, c) ->
-	let decl = (na,Some (substl subst b),substl subst t) in
-	let subst' = mkVar na :: subst in
-	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
-      | Cast (c,_,_)      -> prodec_rec subst l c
-      | _               -> l,c
-  in prodec_rec [] []
       
-let push_named_context = 
-  List.fold_right push_named
-
-let named_of_rel_context (subst, ids, env as init) ctx =
-  Sign.fold_rel_context
-    (fun (na,c,t) (subst, avoid, env) ->
-      let id = Nameops.next_name_away na avoid in
-      let d = (id,Option.map (substl subst) c,substl subst t) in
-	(mkVar id :: subst, id::avoid, d::env))
-    ctx ~init
-    
 let new_class id par ar sup props =
   let env0 = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -294,7 +224,7 @@ let new_class id par ar sup props =
     
   (* Interpret the definitions and propositions *)
   let env_props, prop_impls, bound, ctx_props, _ = 
-    interp_fields_rel_evars isevars env_params bound 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 *)
@@ -344,21 +274,18 @@ let new_class id par ar sup props =
 	      IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
 			     fields (Recordops.lookup_projections kn))
   in
-  let ids = List.map pi1 (named_context env0) in
-  let (subst, ids, named_ctx_params) = named_of_rel_context ([], ids, []) ctx_params in
-  let (_, _, named_ctx_props) = named_of_rel_context (subst, ids, []) ctx_props in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
       match Typeclasses.class_of_constr t with
-      | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d)
+      | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d)
       | None -> (None, d))
-      named_ctx_params
+      ctx_params
   in
   let k =
     { cl_impl = impl;
       cl_params = List.length par;
       cl_context = ctx_context;
-      cl_props = named_ctx_props;
+      cl_props = ctx_props;
       cl_projs = projs }
   in
     declare_implicits (List.rev prop_impls) subs k;
@@ -369,64 +296,15 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
 let binders_of_lidents l =
   List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
 
-let subst_ids_in_named_context subst l =
-  let x, _ = 
-    List.fold_right
-      (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k)
-      l ([], 1)
-  in x
-    
-let subst_one_named inst ids t =
-  substnl inst 0 (substn_vars 1 ids t)
-      
-let subst_named inst subst ctx =
-  let ids = List.map (fun (id, _, _) -> id) subst in
-  let ctx' = subst_ids_in_named_context ids ctx in
-  let ctx', _ =
-    List.fold_right
-      (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
-      ctx' ([], 0)
-  in ctx'
-(*
-let infer_super_instances env params params_ctx super =
-  let super = subst_named params params_ctx super in
-    List.fold_right 
-      (fun (na, _, t) (sups, ids, supctx) -> 
-	let t = subst_one_named sups ids t in
-	let inst = 
-	  try resolve_one_typeclass env t 
-	  with Not_found -> 
-	    let cl, args = destClass t in
-	      no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args)
-	in
-	let d = (na, Some inst, t) in
-	  inst :: sups, na :: ids, d :: supctx)
-      super ([], [], [])*)
-      
-(* let evars_of_context ctx id n env = *)
-(*   List.fold_right (fun (na, _, t) (n, env, nc) ->  *)
-(*     let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *)
-(*     let d = (na, Some b, t) in *)
-(*       (succ n, push_named d env, d :: nc)) *)
-(*     ctx (n, env, []) *)
-
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
+      let t' = substl subst t in
       let c = interp_casted_constr_evars isevars env ce t' in
       let d = na, Some c, t' in
-	(na, c) :: subst, d :: instctx)
+	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-let substitution_of_constrs ctx cstrs =
-  List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
-
-let destClassApp cl =
-  match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
-    | _ -> raise Not_found
-
 let refine_ref = ref (fun _ -> assert(false))
 
 let id_of_class cl =
@@ -521,9 +399,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
   let k, ctx', imps, subst = 
     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
+    let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, List.rev (Array.to_list args)
   in
   let id = 
     match snd instid with
@@ -536,16 +414,16 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  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
+  let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses env !isevars;
   let sigma = Evd.evars_of !isevars in
-  let substctx = Typeclasses.nf_substitution sigma subst in
+  let substctx = List.map (Evarutil.nf_evar sigma) subst in
     if Lib.is_modtype () then
       begin
-	let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in
+	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
-	  let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+	  let t = it_mkProd_or_LetIn ty_constr ctx' in
 	    Evarutil.nf_isevar !isevars t
 	in
 	Evarutil.check_evars env Evd.empty !isevars termtype;
@@ -567,8 +445,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	      List.fold_left
 		(fun (props, rest) (id,_,_) -> 
 		  try 
-		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-		    let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		    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
 		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -579,12 +457,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	      else
 		type_ctx_instance isevars env' k.cl_props props substctx
 	in
-	let app, ty_constr = instance_constructor k (List.rev_map snd subst) in
+	let app, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
-	  let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+	  let t = it_mkProd_or_LetIn ty_constr ctx' in
 	    Evarutil.nf_isevar !isevars t
 	in
-	let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
+	let term = Termops.it_mkLambda_or_LetIn app ctx' in
 	isevars := Evarutil.nf_evar_defs !isevars;
 	let term = Evarutil.nf_isevar !isevars term in
 	let evm = Evd.evars_of (undefined_evars !isevars) in
@@ -607,21 +485,6 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  end
       end
 
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-
-let solve_by_tac env evd evar evi t =
-  let goal = {it = evi; sigma = (Evd.evars_of evd) } in
-  let (res, valid) = t goal in 
-    if res.it = [] then 
-      let prooftree = valid [] in
-      let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in
-	if obls = [] then 
-	  let evd' = evars_reset_evd res.sigma evd in
-	  let evd' = evar_define evar proofterm evd' in
-	    evd', true
-	else evd, false
-    else evd, false
-
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -649,89 +512,3 @@ let context ?(hook=fun _ -> ()) l =
 	     None -> ()
 	   | Some tc -> hook (VarRef id)))
       (List.rev fullctx)
-
-open Libobject
-
-let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")
-let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation")
-  
-let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid)))
-let tactic = lazy (Tacinterp.interp tactic_expr)
-
-let _ =
-  Typeclasses.solve_instanciation_problem :=
-    (fun env evd ev evi -> 
-      Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
-      solve_by_tac env evd ev evi (Lazy.force tactic))
-
-(* let prod = lazy_fun Coqlib.build_prod *)
-
-(* let build_conjunction evm = *)
-(*   List.fold_left *)
-(*     (fun (acc, evs) (ev, evi)  -> *)
-(*       if class_of_constr evi.evar_concl <> None then *)
-(* 	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *)
-(*       else acc, Evd.add evs ev evi) *)
-(*     (Coqlib.build_coq_True (), Evd.empty) evm *)
-
-(* let destruct_conjunction evm_list evm evm' term = *)
-(*   let _, evm = *)
-(*     List.fold_right *)
-(*       (fun (ev, evi) (term, evs) -> *)
-(* 	if class_of_constr evi.evar_concl <> None then *)
-(* 	  match kind_of_term term with *)
-(* 	    | App (x, [| _ ; _ ; proof ; term |]) -> *)
-(* 		let evs' = Evd.define evs ev proof in *)
-(* 		  (term, evs') *)
-(* 	    | _ -> assert(false) *)
-(* 	else *)
-(* 	  match (Evd.find evm' ev).evar_body with *)
-(* 	      Evar_empty -> raise Not_found *)
-(* 	    | Evar_defined c -> *)
-(* 		let evs' = Evd.define evs ev c in *)
-(* 		  (term, evs')) *)
-(*       evm_list (term, evm) *)
-(*   in evm *)
- 
-(* let solve_by_tac env evd evar evi t = *)
-(*   let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
-(*   let (res, valid) = t goal in *)
-(*     if res.it = [] then *)
-(*       let prooftree = valid [] in *)
-(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
-(* 	if obls = [] then *)
-(* 	  let evd' = evars_reset_evd res.sigma evd in *)
-(* 	  let evd' = evar_define evar proofterm evd' in *)
-(* 	    evd', true *)
-(* 	else evd, false *)
-(*     else evd, false *)
-
-(* let resolve_all_typeclasses env evd = *)
-(*   let evm = Evd.evars_of evd in *)
-(*   let evm_list = Evd.to_list evm in *)
-(*   let goal, typesevm = build_conjunction evm_list in *)
-(*   let evars = ref (Evd.create_evar_defs typesevm) in *)
-(*   let term = resolve_one_typeclass_evd env evars goal in *)
-(*   let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *)
-(*     Evd.create_evar_defs evm' *)
-
-(* let _ = *)
-(*   Typeclasses.solve_instanciations_problem := *)
-(*     (fun env evd ->  *)
-(*       Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *)
-(*       resolve_all_typeclasses env evd) *)
-
-let solve_evars_by_tac env evd t =
-  let ev = make_evar empty_named_context_val mkProp in
-  let goal = {it = ev; sigma = (Evd.evars_of evd) } in
-  let (res, valid) = t goal in 
-  let evd' = evars_reset_evd res.sigma evd in
-    evd'
-(*       Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *)
-
-(* let _ = *)
-(*   Typeclasses.solve_instanciations_problem := *)
-(*     (fun env evd ->  *)
-(*       Eauto.resolve_all_evars false (true, 15) env  *)
-(* 	(fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *)
-(* 	  && class_of_constr evi.evar_concl <> None) evd) *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 88147b539..3bc5d0326 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -23,17 +23,24 @@ open Typeclasses
 open Implicit_quantifiers
 (*i*)
 
+(* Errors *)
+
+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 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 option ->
@@ -46,6 +53,10 @@ val default_on_free_vars : identifier list -> unit
 
 val fail_on_free_vars : identifier list -> unit
 
+(* Instance declaration *)
+
+val declare_instance : bool -> identifier located -> unit
+
 val declare_instance_constant :
   typeclass ->
   int option -> (* priority *)
@@ -69,35 +80,14 @@ val new_instance :
   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
-
-val declare_instance : bool -> identifier located -> unit
 
-val mismatched_params : env -> constr_expr list -> named_context -> 'a
+val id_of_class : typeclass -> identifier
 
-val mismatched_props : env -> constr_expr list -> named_context -> 'a
+(* Context command *)    
 
-val solve_by_tac :     env ->
-    Evd.evar_defs ->
-    Evd.evar ->
-  evar_info ->
-  Proof_type.tactic ->
-    Evd.evar_defs * bool
+val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
 
-val solve_evars_by_tac :     env ->
-    Evd.evar_defs ->
-  Proof_type.tactic ->
-  Evd.evar_defs
+(* Forward ref for refine *)
 
 val refine_ref : (open_constr -> Proof_type.tactic) ref
 
-val decompose_named_assum : types -> named_context * types
-
-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 dc9b624fb..9c1c17878 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -536,7 +536,7 @@ let explain_unsatisfiable_constraints env evd constr =
 	
 let explain_mismatched_contexts env c i j = 
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ 
+    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ fnl () ++ brk (1,1) ++ 
     hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
 
 let explain_typeclass_error env err =