Generalize instance declarations to any context, better name handling. Add hole kind info for topconstrs.

Derive eta_expansion from functional extensionality axiom.


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

25 files changed, 328 insertions, 219 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index b1d08f5d2f..28fc7e2906 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -79,16 +79,18 @@ let type_ctx_instance isevars env ctx inst subst =
 	(na, 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 = CHole (dummy_loc) 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 *)
+	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 d = na, Some c, t' in
@@ -98,58 +100,59 @@ let type_class_instance_params isevars env id n ctx inst subst =
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance sup (instid, bk, cl) props =
-  let id, par = Implicit_quantifiers.destClassAppExpl cl in
+let new_instance ctx (instid, bk, cl) props =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let avoid = Termops.ids_of_context env in
-  let k = 
-    try class_info (snd id)
-    with Not_found -> unbound_class env id
-  in
-  let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
-  let gen_ctx = 
-    let is_free ((_, x), _) = 
-      let f l = not (List.exists (fun ((_, y), _) -> y = x) l) in
-      let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in
-	f gen_ctx && g sup
-    in
-    let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) (List.map fst par) in
-    let parbinders' = List.filter is_free parbinders in
-      gen_ctx @ parbinders'
-  in
-  let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
-  let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
-
-  let subst =
-    let cl_context = List.map snd k.cl_context in
+  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
+  let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
+  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 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 
-	      Classes.mismatched_params env (List.map fst par) cl_context;
+	      Classes.mismatched_params env (List.map fst par) (List.map snd k.cl_context);
 	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
 	      (fun avoid (clname, (id, _, t)) -> 
 		match clname with 
-		    Some _ -> CHole (Util.dummy_loc), avoid
+		    Some (cl, b) -> 
+		      let t = 
+			if b then 
+			  let _k = class_info cl in
+			    CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *)
+			else CHole (Util.dummy_loc, None)
+		      in t, avoid
 		  | None -> failwith ("new instance: under-applied typeclass"))
 	      par (List.rev k.cl_context)
-	    in
-	    let subst, _ = type_class_instance_params isevars env' (snd id) 0 cl_context pars [] in
-	      subst
+	    in Topconstr.CAppExpl (Util.dummy_loc, (None, Ident id), pars)
 
-      | Implicit ->
-	  let t' = interp_type_evars isevars env' (Topconstr.CApp (Util.dummy_loc, (None, CRef (Ident id)), par)) in
-	    match kind_of_term t' with 
-		App (c, args) -> 
-		  substitution_of_constrs cl_context
-		    (List.rev (Array.to_list args))
-	      | _ -> assert false
+      | Implicit -> cl
+  in
+  let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
+  let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
+  let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in
+  let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
+  let ctx, avoid = Classes.name_typeclass_binders bound ctx in
+  let ctx = List.rev_append gen_ctx ctx in
+  let k, ctx', subst = 
+    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))
+	| _ -> assert false)
   in
+  let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses ~check:false env sigma !isevars;
+  isevars := resolve_typeclasses env' sigma !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
@@ -167,23 +170,23 @@ let new_instance sup (instid, bk, cl) props =
 	      let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
 	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
 		c :: props, rest'
-	    with Not_found -> (CHole Util.dummy_loc :: props), rest)
+	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 	  ([], props) k.cl_props
       in
 	if rest <> [] then 
-	  unbound_method env k.cl_name (fst (List.hd rest))
+	  unbound_method env' k.cl_name (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 term = it_mkNamedLambda_or_LetIn (it_mkNamedLambda_or_LetIn app supctx) genctx 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 t = it_mkNamedProd_or_LetIn (it_mkNamedProd_or_LetIn app supctx) genctx in
+    let t = it_mkNamedProd_or_LetIn app ctx' in
       Evarutil.nf_isevar !isevars t
   in
   isevars := undefined_evars !isevars;
@@ -191,22 +194,19 @@ let new_instance sup (instid, bk, cl) props =
     match snd instid with
 	Name id -> id
       | Anonymous -> 
-	  let i = Nameops.add_suffix (snd id) "_instance_" in
+	  let i = Nameops.add_suffix k.cl_name "_instance_" in
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
   let imps = 
     Util.list_map_i 
       (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
-      1 (genctx @ List.rev supctx)
+      1 ctx'
   in
   let hook cst = 
     let inst = 
       { is_class = k;
 	is_name = id;
-(* 	is_params = paramsctx; *)
-(* 	is_super = superctx; *)
 	is_impl = cst;
-(* 	is_add_hint = (fun () -> Classes.add_instance_hint id); *)
       }
     in
       Classes.add_instance_hint id;
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index ce4b32cad8..f9b36b0c06 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -33,7 +33,7 @@ val type_ctx_instance :     Evd.evar_defs ref ->
     (Names.identifier * Term.constr option * Term.constr) list
 
 val new_instance : 
-  typeclass_context ->
+  Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
   unit
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 06edeaed20..69d5ad67a9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -651,13 +651,13 @@ let rec extern inctx scopes vars r =
 
   | RVar (loc,id) -> CRef (Ident (loc,id))
 
-  | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
+  | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
 
   | REvar (loc,n,l) ->
       extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
 
   | RPatVar (loc,n) ->
-      if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
+      if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
 
   | RApp (loc,f,args) ->
       (match f with
@@ -756,7 +756,7 @@ let rec extern inctx scopes vars r =
 
   | RSort (loc,s) -> CSort (loc,extern_rawsort s)
 
-  | RHole (loc,e) -> CHole loc
+  | RHole (loc,e) -> CHole (loc, Some e)
 
   | RCast (loc,c, CastConv (k,t)) ->
       CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 033052325a..b2c7728fdb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -923,8 +923,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let env'' = List.fold_left (push_name_env lvar) env ids in
         let p' = Option.map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole loc -> 
-	RHole (loc, Evd.QuestionMark true)
+    | CHole (loc, k) -> 
+	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 162591872b..112c2fc189 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -25,16 +25,8 @@ open Typeclasses
 open Typeclasses_errors
 (*i*)
 
-(* Auxilliary functions for the inference of implicitly quantified variables. *)    
-
-let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
-  let found id bdvars l = if Idset.mem id bdvars then l else if List.mem id l then l else id :: l in
-  let rec aux bdvars l c = match c with
-    | CRef (Ident (_,id)) -> found id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
-	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
-    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
-  in aux bound l c
+let ids_of_list l = 
+  List.fold_right Idset.add l Idset.empty
 
 
 let locate_reference qid =
@@ -59,6 +51,39 @@ let is_freevar ids env x =
       with _ -> not (is_global x)
   with _ -> true
 
+(* Auxilliary functions for the inference of implicitly quantified variables. *)    
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
+  let found id bdvars l = 
+    if List.mem id l then l 
+    else if not (is_freevar bdvars (Global.env ()) id)
+    then l else id :: l 
+  in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident (_,id)) -> found id bdvars l
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+  in aux bound l c
+
+let ids_of_names l = 
+  List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = 
+  let rec aux bdvars l c = match c with
+      ((LocalRawAssum (n, _, c)) :: tl) ->
+	let bound = ids_of_names n in
+	let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+    | ((LocalRawDef (n, c)) :: tl) -> 
+	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+	let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+	
+    | [] -> bdvars, l
+  in aux bound l binders
+
 let rec make_fresh ids env x =
   if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
 
@@ -82,7 +107,10 @@ let compute_constrs_freevars env constrs =
 
 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) elts
+    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 = *)
@@ -139,9 +167,6 @@ let destClassAppExpl cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, l
     | _ -> raise Not_found
 
-let ids_of_list l = 
-  List.fold_right Idset.add l Idset.empty
-
 let full_class_binders env l = 
   let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
   let l', avoid =
@@ -184,7 +209,7 @@ let resolve_class_binders env l =
   let ctx = full_class_binders env l in
   let fv_ctx = 
     let elts = compute_context_freevars env ctx in
-      List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
   in
     fv_ctx, ctx
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 3e26b6c72a..ab23e763c1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -23,6 +23,7 @@ open Util
 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
 
@@ -30,6 +31,13 @@ val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
   Names.identifier list -> Names.identifier list
 
+val binder_list_of_ids : identifier list -> local_binder list
+
+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 -> 
@@ -51,10 +59,10 @@ val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> Names.identifier option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (Names.identifier * 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 option * Term.named_declaration) list ->
+  ((Names.identifier * bool) option * Term.named_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index aa3c923ebf..97a0f94da5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -565,7 +565,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc
+  | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
@@ -633,7 +633,7 @@ let constr_loc = function
   | CCases (loc,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
-  | CHole loc -> loc
+  | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_,_) -> loc
   | CSort (loc,_) -> loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index fa7940faa8..6bbc64cca2 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,7 +125,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc
+  | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
@@ -146,6 +146,7 @@ and recursion_order_expr =
   | CWfRec of constr_expr
   | CMeasureRec of constr_expr
 
+(** Anonymous defs allowed ?? *)
 and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * binder_kind * constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bd6c15ffaa..e55024b516 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole loc in
+    | None -> CHole (loc, None) in
   (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
@@ -65,7 +65,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
        Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole loc in
+    | None -> CHole (loc, None) in
   (snd id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
@@ -102,7 +102,7 @@ let lpar_id_coloneq =
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let typeclass_constraint pattern;
+  binder binder_let binders_let delimited_binder_let delimited_binders_let typeclass_constraint pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -222,7 +222,7 @@ GEXTEND Gram
       | s=sort -> CSort (loc,s)
       | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (loc, String s)
-      | "_" -> CHole loc
+      | "_" -> CHole (loc, None)
       | id=pattern_ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
@@ -311,33 +311,59 @@ GEXTEND Gram
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
-          LocalRawAssum (idl,Default Explicit,CHole loc)::bl
+          LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
       | idl=LIST1 name; ":"; c=lconstr -> 
           [LocalRawAssum (idl,Default Explicit,c)]
       | cl = binders_let -> cl
     ] ]
   ;
+  delimited_binders_let: 
+    [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
+	  ctx @ bl
+    | b = delimited_binder_let; cl = LIST0 binder_let -> b :: cl
+    | -> [] ] ]
+  ;
   binders_let: 
     [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
 	  ctx @ bl
-    | cl = LIST0 binder_let -> cl
-    ] ]
+    | cl = LIST0 binder_let -> cl ] ]
   ;
   binder_let:
     [ [ id=name ->
-          LocalRawAssum ([id],Default Explicit,CHole loc)
+          LocalRawAssum ([id],Default Explicit,CHole (loc, None))
       | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
           LocalRawAssum (id::idl,Default Explicit,c)
       | "("; id=name; ":"; c=lconstr; ")" -> 
           LocalRawAssum ([id],Default Explicit,c)
       | "`"; id=name; "`" ->
-          LocalRawAssum ([id],Default Implicit,CHole loc)
+          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
+      | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,c)
+      | "`"; id=name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum ([id],Default Implicit,c)
+      | "`"; id=name; idl=LIST1 name; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
+      | "("; id=name; ":="; c=lconstr; ")" ->
+          LocalRawDef (id,c)
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
+          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
+      | "["; tc = typeclass_constraint_binder; "]" -> tc
+    ] ]
+(*     | b = delimited_binder_let -> b ] ] *)
+  ;
+  delimited_binder_let:
+    [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum (id::idl,Default Explicit,c)
+      | "("; id=name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum ([id],Default Explicit,c)
+      | "`"; id=name; "`" ->
+          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
       | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
           LocalRawAssum (id::idl,Default Implicit,c)
       | "`"; id=name; ":"; c=lconstr; "`" -> 
           LocalRawAssum ([id],Default Implicit,c)
       | "`"; id=name; idl=LIST1 name; "`" -> 
-          LocalRawAssum (id::idl,Default Implicit,CHole loc)
+          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
@@ -346,7 +372,7 @@ GEXTEND Gram
     ] ]
   ;
   binder:
-    [ [ id=name -> ([id],Default Explicit,CHole loc)
+    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
       | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
       | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c) 
     ] ]
@@ -358,11 +384,11 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ id=identref ; cl = LIST1 typeclass_param -> 
+    [ [ id=identref ; cl = LIST0 typeclass_param -> 
       (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | "?" ; id=identref ; cl = LIST1 typeclass_param -> 
+    | "?" ; id=identref ; cl = LIST0 typeclass_param -> 
 	(loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST1 typeclass_param -> 
+    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST0 typeclass_param -> 
 	(fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 540d1aac0b..b69a6a97ac 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -286,7 +286,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
-      | -> CHole loc ] ]
+      | -> CHole (loc, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -314,7 +314,7 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-    [ [ id = name -> (false,AssumExpr(id,CHole loc))
+    [ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
       | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
       | id = name; oc = of_type_with_opt_coercion;
@@ -339,7 +339,7 @@ GEXTEND Gram
         coe = of_type_with_opt_coercion; c = lconstr ->
 	  (coe,(id,mkCProdN loc l c))
       | id = identref; l = LIST0 binder_let ->
-	  (false,(id,mkCProdN loc l (CHole loc))) ] ]
+	  (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true
@@ -479,7 +479,7 @@ GEXTEND Gram
 	   VernacClass (qid, pars, s, [], props)
 
       (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
+      | IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ];
 	 qid = identref; pars = binders_let;
 	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
 	 props = typeclass_field_types ->
@@ -488,7 +488,7 @@ GEXTEND Gram
       | IDENT "Context"; c = typeclass_context -> 
 	  VernacContext c
 
-      | IDENT "Instance"; sup = OPT [ l = typeclass_context ; "=>" -> l ];
+      | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
 	 is = typeclass_constraint ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
 	     VernacInstance (sup, is, props)
@@ -525,7 +525,7 @@ GEXTEND Gram
   ;
 (*   typeclass_param_type: *)
 (*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
-(*     | id = identref -> id, CHole loc ] ] *)
+(*     | id = identref -> id, CHole (loc, None) ] ] *)
 (*   ; *)
   typeclass_field_type:
     [ [ id = identref; ":"; t = lconstr -> id, t ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2430b88636..68ddc19292 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -434,7 +434,9 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
+    let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
+    let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 89bdf13ebd..d5cffd35bd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,7 +163,9 @@ module Constr :
     val lconstr_pattern : constr_expr Gram.Entry.e
     val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
     val binder_let : local_binder Gram.Entry.e
+    val delimited_binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
+    val delimited_binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ed4386ada0..8dff6dbf53 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -239,7 +239,7 @@ let pr_binder_among_many pr_c = function
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, CastConv (_,t)) -> c, t
-        | _ -> c, CHole dummy_loc in
+        | _ -> c, CHole (dummy_loc, None) in
       hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0b889bf08d..e2653a9606 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -263,7 +263,7 @@ let rec pr_module_expr = function
       hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
 let pr_type_option pr_c = function
-  | CHole loc -> mt()
+  | CHole (loc, k) -> mt()
   | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
 let pr_decl_notation prc =
@@ -399,12 +399,6 @@ let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
 let pr_lname_lident_constr (oi,bk,a) = 
   (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) 
   ++ pr_lconstr a in
-let pr_typeclass_context l = 
-  match l with
-      [] -> mt ()
-    | _ -> str"[" ++ spc () ++ prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l
-	++ spc () ++ str"]" ++ spc ()
-in
 let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
   ++ sep ++ pr_constrarg c in
 
@@ -706,7 +700,7 @@ let rec pr_vernac = function
  | VernacInstance (sup, (instid, bk, cl), props) -> 
      hov 1 (
        str"Instance" ++ spc () ++ 
-	 pr_typeclass_context sup ++
+	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++ 
 	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
 	 pr_constr_expr cl ++ spc () ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6fdfba23d3..26dff3927a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -154,7 +154,8 @@ let rec mlexpr_of_constr = function
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
+  | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
+  | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
   | Topconstr.CNotation(_,ntn,l) ->
       <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
                 $mlexpr_of_list mlexpr_of_constr l$ >>
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3689ae174a..c9d44e3dc9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -670,6 +670,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
+    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e253410dee..a1183c97bb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -33,7 +33,7 @@ type typeclass = {
   cl_name : identifier;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (identifier option * named_declaration) list; 
+  cl_context : ((identifier * bool) option * named_declaration) list; 
 
   cl_params: int;
 
@@ -298,13 +298,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
   in sat evd
 
 let class_of_constr c = 
-  match kind_of_term c with
-      App (c, _) -> 
-	(match kind_of_term c with
-	    Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
-	  | _ -> None)
-    | _ -> None
-
+  let extract_ind c =
+    match kind_of_term c with
+	Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
+      | _ -> None
+  in
+    match kind_of_term c with
+	App (c, _) -> extract_ind c
+      | _ -> extract_ind c
 
 type substitution = (identifier * constr) list
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 47cb93a149..ec3350a586 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -26,8 +26,9 @@ type typeclass = {
   (* Name of the class. FIXME: should not necessarily be globally unique. *)
   cl_name : identifier;
 
-  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (identifier option * named_declaration) list; 
+  (* 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_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
 
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index fee38a6292..b05b7ec8c2 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -67,14 +67,14 @@ let arrow_morphism a b =
 	   mkLambda (Name (id_of_string "B"), b, 
 		    mkProd (Anonymous, mkRel 2, mkRel 2)))
     
-let setoid_refl l sa x = 
-  applistc (Lazy.force setoid_refl_proj) (l @ [sa ; x])
+let setoid_refl pars x = 
+  applistc (Lazy.force setoid_refl_proj) (pars @ [x])
       
 let class_one = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
 let class_two = lazy (Lazy.force morphism2_class, Lazy.force respect2_proj)
 let class_three = lazy (Lazy.force morphism3_class, Lazy.force respect3_proj)
 
-exception Found of (constr * constant * constr list * int * constr * constr array *
+exception Found of (constr * constant * constr list * constr * constr array *
 		       (constr * (constr * constr * constr * constr * constr)) option array)
 
 let resolve_morphism_evd env evd app = 
@@ -90,7 +90,7 @@ let is_equiv env sigma t =
 
 let resolve_morphism env sigma direction oldt m args args' = 
   let evars = ref (Evd.create_evar_defs Evd.empty) in
-  let morph_instance, proj, subst, len, m', args, args' = 
+  let morph_instance, proj, subst, m', args, args' = 
     if is_equiv env sigma m then 
       let params, rest = array_chop 3 args in
       let a, r, s = params.(0), params.(1), params.(2) in
@@ -98,15 +98,14 @@ let resolve_morphism env sigma direction oldt m args args' =
       let inst = mkApp (Lazy.force setoid_morphism, params) in
 	(* Equiv gives a binary morphism *)
       let (cl, proj) = Lazy.force class_two in
-      let ctxargs = [ a; r; a; r; mkProp; Lazy.force iff; s; s; Lazy.force iff_setoid; ] in
+      let ctxargs = [ a; r; s; a; r; s; mkProp; Lazy.force iff; Lazy.force iff_setoid; ] in
       let m' = mkApp (m, [| a; r; s |]) in
-	inst, proj, ctxargs, 6, m', rest, rest'
+	inst, proj, ctxargs, m', rest, rest'
     else
       let cls =
 	match Array.length args with
 	    1 -> [Lazy.force class_one, 1]
 	  | 2 -> [Lazy.force class_two, 2; Lazy.force class_one, 1]
-	  | 3 -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1]
 	  | n -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1]
       in
 	try 
@@ -114,8 +113,6 @@ let resolve_morphism env sigma direction oldt m args args' =
 	    evars := Evd.create_evar_defs Evd.empty;
 	    let cl_param, cl_context = match cl.cl_context with hd :: tl -> hd, tl | [] -> assert false in
 	    let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] (List.map snd cl_context) in
-	    let len = List.length ctxevs in
-(* 	    let superevs = substitution_of_named_context evars env cl.cl_name len ctxevs cl.cl_super in *)
 	    let morphargs, morphobjs = array_chop (Array.length args - n) args in
 	    let morphargs', morphobjs' = array_chop (Array.length args - n) args' in
 	    let args = List.rev_map (fun (_, c) -> c) ctxevs in
@@ -124,11 +121,12 @@ let resolve_morphism env sigma direction oldt m args args' =
 	    let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in
 	    let mtype = replace_vars ctxevs (pi3 (snd cl_param)) in
 	      try 
-		evars := Unification.w_unify true env CONV ~mod_delta:true appmtype mtype !evars;
+		evars := Evarconv.the_conv_x env appmtype mtype !evars;
 		evars := Evarutil.nf_evar_defs !evars;
 		let app = Evarutil.nf_isevar !evars app in
-		  raise (Found (resolve_morphism_evd env evars app, proj, args, len, appm, morphobjs, morphobjs'))
+		  raise (Found (resolve_morphism_evd env evars app, proj, args, appm, morphobjs, morphobjs'))
 	      with Not_found -> ()
+		| Reduction.NotConvertible -> ()
 		| Stdpp.Exc_located (_, Pretype_errors.PretypeError _) 
 		| Pretype_errors.PretypeError _ -> ())
 	    cls; 
@@ -138,28 +136,27 @@ let resolve_morphism env sigma direction oldt m args args' =
   evars := Evarutil.nf_evar_defs !evars;
   let evm = Evd.evars_of !evars in
   let ctxargs = List.map (Reductionops.nf_evar evm) subst in
-  let ctx, sup = Util.list_chop len ctxargs in
+(*   let ctx, sup = Util.list_chop len ctxargs in *)
   let m' = Reductionops.nf_evar evm m' in
   let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in
-  let projargs, respars, ressetoid, typeargs = 
+  let projargs, respars, typeargs = 
     array_fold_left2 
-      (fun (acc, ctx, sup, typeargs') x y -> 
-	let par, ctx = list_chop 2 ctx in
-	let setoid, sup = List.hd sup, List.tl sup in
+      (fun (acc, ctxargs, typeargs') x y -> 
+	let par, ctx = list_chop 3 ctxargs in
 	  match y with
 	      None ->
-		let refl_proof = setoid_refl par setoid x in
-		  [ refl_proof ; x ; x ] @ acc, ctx, sup, x :: typeargs'
+		let refl_proof = setoid_refl par x in
+		  [ refl_proof ; x ; x ] @ acc, ctx, x :: typeargs'
 	    | Some (p, (_, _, _, _, t')) ->
 		if direction then
-		  [ p ; t'; x ] @ acc, ctx, sup, t' :: typeargs'
-		else [ p ; x; t' ] @ acc, ctx, sup, t' :: typeargs')
-      ([], ctx, sup, []) args args'
+		  [ p ; t'; x ] @ acc, ctx, t' :: typeargs'
+		else [ p ; x; t' ] @ acc, ctx, t' :: typeargs')
+      ([], ctxargs, []) args args'
   in
   let proof = applistc appproj (List.rev projargs) in
   let newt = applistc m' (List.rev typeargs) in
-    match respars, ressetoid with
-	[ a ; r ], [ s ] -> (proof, (a, r, s, oldt, newt))
+    match respars with
+	[ a ; r ; s ] -> (proof, (a, r, s, oldt, newt))
       | _ -> assert(false)
       
 let build_new gl env setoid direction origt newt hyp hypinfo concl =
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 000cf70a35..c3f2413073 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -90,10 +90,6 @@ Ltac setoid_refl :=
   match goal with
     | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
     | [ H : ?X =!= ?X |- _ ] => elim H ; setoid_refl
-    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
-    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
-    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
-    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
   end.
 
 Ltac setoid_sym := 
@@ -161,7 +157,7 @@ Ltac setoidify := repeat setoidify_tac.
 Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop :=
   forall x y, eqa x y -> eqb (m x) (m y).
 
-Class [ Setoid a eqa, Setoid b eqb ] => Morphism (m : a -> b) :=
+Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => Morphism (m : a -> b) :=
   respect : respectful m.
 
 (** Here we build a setoid instance for functions which relates respectful ones only. *)
@@ -209,7 +205,7 @@ Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d e
 Program Instance iff_setoid : Setoid Prop iff :=
   equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
 
-(* Program Instance not_morphism : Morphism Prop iff Prop iff not. *)
+Program Instance not_morphism : Morphism Prop iff Prop iff not.
 
 Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
 
@@ -272,13 +268,13 @@ Proof.
 Qed.
 
 Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
-  ? Morphism sb sc g, ? Morphism sa sb f ] => 
+  mg : ? Morphism sb sc g, mf : ? Morphism sa sb f ] => 
   compose_morphism : ? Morphism sa sc (fun x => g (f x)).
 
 Next Obligation.
 Proof.
-  apply (respect (m0:=m)).
-  apply (respect (m0:=m0)).
+  apply (respect (m0:=mg)).
+  apply (respect (m0:=mf)).
   assumption.
 Qed.
 
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 81bb5390b1..e890261e12 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -30,17 +31,6 @@ Proof.
   auto.
 Qed.
 
-(** Eta expansion *)
-
-Axiom eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
-  f = fun x => f x.
-
-Lemma eta_expansion : forall A B (f : A -> B), 
-  f = fun x => f x.
-Proof.
-  intros ; apply eta_expansion_dep.
-Qed.
-
 (** Statements of functional equality for simple and dependent functions. *)
 
 Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), 
@@ -63,6 +53,22 @@ Tactic Notation "extensionality" ident(x) :=
     [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x
   end.
 
+(** Eta expansion follows from extensionality. *)
+
+Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
+  f = fun x => f x.
+Proof.
+  intros.
+  extensionality x.
+  reflexivity.
+Qed.
+  
+Lemma eta_expansion : forall A B (f : A -> B), 
+  f = fun x => f x.
+Proof.
+  intros ; apply eta_expansion_dep.
+Qed.
+
 (** The two following lemmas allow to unfold a well-founded fixpoint definition without
    restriction using the functional extensionality axiom. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index a2eab577d1..3eb9a30894 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -113,8 +113,10 @@ let declare_implicits impls cl =
       list_fold_left_i 
 	(fun i acc (is, (na, b, t)) -> 
 	  if len - i <= cl.cl_params then acc
-	  else if is = None then (ExplByPos (i, Some na), (false, true)) :: acc
-	  else 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
@@ -175,29 +177,55 @@ let interp_fields_evars isevars env avoid l =
       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, i :: ids, d::params, ([], data :: snd impls)))
+	(push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
     (env, [], avoid, [], ([], [])) l    
 
-let decompose_typeclass_prod env avoid = 
-  let rec prodec_rec subst env avoid l c =
+let name_typeclass_binder avoid = function
+  | LocalRawAssum ([loc, Anonymous], bk, c) ->
+      let name = 
+	let id = 
+	match c with
+	    CApp (_, (_, CRef (Ident (loc,id))), _) -> id
+	  | _ -> id_of_string "assum"
+	in Implicit_quantifiers.make_fresh avoid (Global.env ()) id
+      in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid
+  | x -> x, avoid
+
+let name_typeclass_binders avoid l = 
+  let l', avoid = 
+    List.fold_left 
+      (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in
+				   b' :: binders, avoid)
+      ([], avoid) l
+  in List.rev l', avoid
+
+let decompose_named_assum = 
+  let rec prodec_rec subst l c =
     match kind_of_term c with
-    | Prod (x,t,c) ->
-	let name = id_of_name_using_hdchar env c x in
-	let name = Nameops.next_ident_away_from name avoid in
-	let decl = (name,None,substl subst t) in
-	  prodec_rec (mkVar name :: subst) (push_named decl env) (name :: avoid) (add_named_decl decl l) c
-(*     | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c *)
-    | Cast (c,_,_)      -> prodec_rec subst env avoid l c
-    | _               -> l,c
-  in 
-  prodec_rec [] env avoid []
-
+      | 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)
+      | Cast (c,_,_)      -> prodec_rec subst l c
+      | _               -> l,c
+  in prodec_rec [] []
+      
 let push_named_context = List.fold_right push_named
 
 let new_class id par ar sup props =
   let env0 = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let avoid = Termops.ids_of_context env0 in
+  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in
+  let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in
+  let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in
+  let sup, bound = name_typeclass_binders bound sup in
+  let supnames = 
+    List.fold_left (fun acc b -> 
+      match b with
+	  LocalRawAssum (nl, _, _) -> nl @ acc
+	| LocalRawDef _ -> assert(false))
+      [] sup
+  in
 
   (* Interpret the arity *)
   let arity_imps, fullarity = 
@@ -205,12 +233,12 @@ let new_class id par ar sup props =
     let term = prod_constr_expr (prod_constr_expr arity par) sup in
       interp_type_evars isevars env0 term      
   in
-  let ctx_params, arity = decompose_typeclass_prod env0 avoid fullarity in
+  let ctx_params, arity = decompose_named_assum fullarity in
   let env_params = push_named_context ctx_params env0 in
     
   (* Interpret the definitions and propositions *)
-  let env_props, prop_impls, avoid, ctx_props, _ = 
-    interp_fields_evars isevars env_params avoid props 
+  let env_props, prop_impls, bound, ctx_props, _ = 
+    interp_fields_evars isevars env_params bound props 
   in
     
   (* Instantiate evars and check all are resolved *)
@@ -230,8 +258,8 @@ let new_class id par ar sup props =
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
       match Typeclasses.class_of_constr t with
-	  None -> (None, d)
-	| Some cl -> (Some cl.cl_name, d))
+	| Some cl -> (Some (cl.cl_name, List.exists (fun (_, n) -> n = Name na) supnames), d)
+	| None -> (None, d))
       ctx_params
   in
   let k =
@@ -258,7 +286,7 @@ let declare_instance (_,id) =
 type binder_def_list = (identifier located * identifier located list * constr_expr) list
 
 let binders_of_lidents l =
-  List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole loc)) 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, _ = 
@@ -326,41 +354,55 @@ let destClassApp cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
     | _ -> raise Not_found
 
-let new_instance sup (instid, bk, cl) props =
-  let id, par = destClassApp cl in
+let new_instance ctx (instid, bk, cl) props =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let avoid = Termops.ids_of_context env in
-  let k = 
-    try class_info (snd id)
-    with Not_found -> unbound_class env id
-  in
-  let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
-  let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
-  let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
-  let subst = 
+
+  let tclass = 
     match bk with
-	Explicit ->
-	  if List.length par <> List.length (List.filter (fun (x, y) -> x <> None) k.cl_context) then 
-	    mismatched_params env par (List.map snd k.cl_context);
-	  let cl_context = List.map snd k.cl_context in
-	  let len = List.length cl_context in
-	  let ctx, par = Util.list_chop len par in
-	  let subst, _ = type_ctx_instance isevars env' cl_context ctx [] in
-	    subst
-
-      | Implicit ->
-	  let _imps, t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in
-	    match kind_of_term t' with 
-		App (c, args) -> 
-		  substitution_of_constrs (List.map snd k.cl_context)
-		    (List.rev (Array.to_list args))
-	      | _ -> assert false
+      | 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 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 
+	      mismatched_params env (List.map fst par) (List.map snd k.cl_context);
+	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
+	      (fun avoid (clname, (id, _, t)) -> 
+		match clname with 
+		    Some (cl, b) -> 
+		      let t = 
+			if b then 
+			  let _k = class_info cl in
+			    CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *)
+			else CHole (Util.dummy_loc, None)
+		      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)
+
+      | Implicit -> cl
   in
+  let k, ctx', subst = 
+    let c = abstract_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))
+	| _ -> assert false)
+  in
+  let env' = push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
+  isevars := resolve_typeclasses env sigma !isevars;
+  let sigma = Evd.evars_of !isevars in
   let env' = Implicit_quantifiers.nf_env sigma env' in
-  let subst = Typeclasses.nf_substitution sigma subst in 
+  let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, propsctx = 
     let props = 
       List.map (fun (x, l, d) -> 
@@ -369,12 +411,12 @@ let new_instance sup (instid, bk, cl) props =
     in
       if List.length props <> List.length k.cl_props then 
 	mismatched_props env' props k.cl_props;
-      type_ctx_instance isevars env' k.cl_props props subst
+      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 term = Termops.it_mkNamedLambda_or_LetIn (Termops.it_mkNamedLambda_or_LetIn app supctx) genctx 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 cdecl = 
@@ -391,7 +433,7 @@ let new_instance sup (instid, bk, cl) props =
       match snd instid with
 	  Name id -> id
 	| Anonymous -> 
-	    let i = Nameops.add_suffix (snd id) "_instance_" in
+	    let i = Nameops.add_suffix k.cl_name "_instance_" in
 	      Termops.next_global_ident_away false i (Termops.ids_of_context env)
     in
       instid, Declare.declare_constant instid cdecl
@@ -399,10 +441,7 @@ let new_instance sup (instid, bk, cl) props =
   let inst = 
     { is_class = k;
       is_name = id;
-(*       is_params = paramsctx; (\* missing gen_ctx *\) *)
-(*       is_super = superctx; *)
       is_impl = cst;
-(*       is_add_hint = (fun () -> add_instance_hint id); *)
     }
   in
     add_instance_hint id;
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 5855759b24..7956089777 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -40,7 +40,7 @@ val new_class : identifier located ->
   binder_list -> unit
 
 val new_instance : 
-  typeclass_context ->
+  local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
   unit
@@ -63,3 +63,11 @@ val solve_by_tac :     env ->
   evar_info ->
   Proof_type.tactic ->
     Evd.evar_defs * bool
+
+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/command.ml b/toplevel/command.ml
index 445555251e..9ccd2ff2e6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -83,7 +83,7 @@ let rec destSubCast c = match kind_of_term c with
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
   | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
-  | CHole loc ->
+  | CHole (loc, k) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
 	user_err_loc (loc,"",
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 02517ae96e..b2b648a665 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -233,7 +233,7 @@ type vernac_expr =
 	(lident * constr_expr) list (* props *)
 	
   | VernacInstance of
-      typeclass_context * (* super *)
+      local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(lident * lident list * constr_expr) list (* props *)