A much better implementation of implicit generalization:

- Do it after internalisation (esp. after notation expansion)
- Generalize it to any constr, not just typeclasses
- Prepare for having settings on the implicit status of generalized
variables (currently only impl,impl and expl,expl are supported).
- Simplified implementation! (Still some refactoring needed in
typeclasses parsing code).
This patch contains a fix for bug #1964 as well.


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

5 files changed, 187 insertions, 187 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2faa866220..9b8f62aa03 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -178,7 +178,7 @@ let contract_pat_notation ntn (l,ll) =
 
 let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
 
-let set_var_scope loc id (_,scopt,scopes) varscopes =
+let set_var_scope loc id (_,_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
   if !idscopes <> None & 
     make_current_scope (Option.get !idscopes)
@@ -191,11 +191,11 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder (subst,substlist) (renaming,(ids,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
+    (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -212,8 +212,8 @@ let rec subst_iterator y t = function
   | x -> map_rawconstr (subst_iterator y t) x
 
 let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
-  let (renaming,(ids,_,scopes)) = infos in
-  let subinfos = renaming,(ids,None,scopes) in
+  let (renaming,(ids,unb,_,scopes)) = infos in
+  let subinfos = renaming,(ids,unb,None,scopes) in
   match c with
   | AVar id ->
       begin
@@ -221,7 +221,7 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
 	(* of the notations *)
 	try 
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	  interp (ids,scopt,subscopes@scopes) a
+	  interp (ids,unb,scopt,subscopes@scopes) a
 	with Not_found -> 
 	try 
 	  RVar (loc,List.assoc id renaming)
@@ -246,7 +246,7 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
       rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
       (subst_aconstr_in_rawconstr loc interp sub) subinfos t
 
-let intern_notation intern (_,tmp_scope,scopes as env) loc ntn fullargs =
+let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
   let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
   let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
   Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) df;
@@ -254,11 +254,11 @@ let intern_notation intern (_,tmp_scope,scopes as env) loc ntn fullargs =
   let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
   subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
 
-let set_type_scope (ids,tmp_scope,scopes) =
-  (ids,Some Notation.type_scope,scopes)
+let set_type_scope (ids,unb,tmp_scope,scopes) =
+  (ids,unb,Some Notation.type_scope,scopes)
 
-let reset_tmp_scope (ids,tmp_scope,scopes) =
-  (ids,None,scopes)
+let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
+  (ids,unb,None,scopes)
 
 let rec it_mkRProd env body =
   match env with
@@ -282,7 +282,7 @@ let string_of_ty = function
   | Recursive -> "def"
   | Method -> "meth"
 
-let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
+let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
@@ -291,12 +291,12 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
     let tys = string_of_ty ty in
       Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
-    RVar (loc,id), impl, argsc, l
+      RVar (loc,id), impl, argsc, l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
   then
-      RVar (loc,id), [], [], []
+    RVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
@@ -310,17 +310,17 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
 	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
-  (* Is [id] a goal or section variable *)
-  let _ = Sign.lookup_named id vars2 in
-  try
-    (* [id] a section variable *)
-    (* Redundant: could be done in intern_qualid *)
-    let ref = VarRef id in
-    RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
-  with _ ->
-    (* [id] a goal variable *)
-    RVar (loc,id), [], [], []
-
+    (* Is [id] a goal or section variable *)
+    let _ = Sign.lookup_named id vars2 in
+      try
+	(* [id] a section variable *)
+	(* Redundant: could be done in intern_qualid *)
+	let ref = VarRef id in
+	  RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+      with _ ->
+	(* [id] a goal variable *)
+	RVar (loc,id), [], [], []
+	    
 let find_appl_head_data (_,_,_,(_,impls)) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
@@ -359,10 +359,10 @@ let intern_non_secvar_qualid loc qid intern env args =
     | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
-let intern_applied_reference intern env lvar args = function
+let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
   | Qualid (loc, qid) ->
       let r,args2 = intern_qualid loc qid intern env args in
-      find_appl_head_data lvar r, args2
+	find_appl_head_data lvar r, args2
   | Ident (loc, id) ->
       try intern_var env lvar loc id, args
       with Not_found -> 
@@ -372,18 +372,19 @@ let intern_applied_reference intern env lvar args = function
 	find_appl_head_data lvar r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
-	if !interning_grammar then (RVar (loc,id), [], [], []),args
+	if !interning_grammar || unb then
+	  (RVar (loc,id), [], [], []),args
 	else raise e
-
+	  
 let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
-      (Idset.empty,None,[]) (vars,[],[],([],[])) [] r
+      (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r
   in r
 
-let apply_scope_env (ids,_,scopes) = function
-  | [] -> (ids,None,scopes), []
-  | sc::scl -> (ids,sc,scopes), scl
+let apply_scope_env (ids,unb,_,scopes) = function
+  | [] -> (ids,unb,None,scopes), []
+  | sc::scl -> (ids,unb,sc,scopes), scl
 
 let rec adjust_scopes env scopes = function
   | [] -> []
@@ -679,46 +680,55 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
     pr_id id ++ strbrk " must not be used as a bound variable in the type \
 of its constructor.")
 
-let push_name_env lvar (ids,tmpsc,scopes as env) = function
+let push_name_env lvar (ids,unb,tmpsc,scopes as env) = function
   | Anonymous -> env 
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
-      (Idset.add id ids,tmpsc,scopes)
+      (Idset.add id ids, unb,tmpsc,scopes)
 
-let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
+let push_loc_name_env lvar (ids,unb,tmpsc,scopes as env) loc = function
   | Anonymous -> env 
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
       Dumpglob.dump_binding loc id;
-      (Idset.add id ids,tmpsc,scopes)
-
-let intern_typeclass_binders intern_type lvar env bl =
-  List.fold_left 
-    (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) ->
-      let env = push_loc_name_env lvar env loc na in
-      let ty = locate_if_isevar loc na (intern_type env ty) in
-	(env, (na,bk,None,ty)::bl))
-    env bl
-
-let intern_typeclass_binder intern_type lvar (env,bl) cb =
-  let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
-    intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
-    
-let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
+      (Idset.add id ids,unb,tmpsc,scopes)
+
+let intern_generalized_binder intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
+  let ty = 
+    if t then ty else
+      let is_class =
+	try
+	  let (loc, r, _ as clapp) = Implicit_quantifiers.destClassAppExpl ty in
+	  let (loc, qid) = qualid_of_reference r in
+	  let gr = Nametab.locate qid in
+	    if Typeclasses.is_class gr then Some (clapp, gr) else None
+	with Not_found -> None
+      in 
+	match is_class with
+	| None -> ty
+	| Some (clapp, gr) -> Implicit_quantifiers.full_class_binder ids clapp gr
+  in
+  let ty = intern_type (ids,true,tmpsc,sc) ty in
+  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty in
+  let env' = List.fold_left (fun env (x, l) -> push_loc_name_env lvar env l (Name x)) env fvs in
+  let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
+    (push_loc_name_env lvar env' loc na), (na,b',None,ty) :: List.rev bl
+      
+let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
-	| Default k ->
-	    let (loc,na) = List.hd nal in
-	      (* TODO: fail if several names with different implicit types *)
-	    let ty = locate_if_isevar loc na (intern_type env ty) in
-	      List.fold_left
-		(fun ((ids,ts,sc),bl) (_,na) ->
-		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
-		(env,bl) nal
-	| TypeClass (b,b') ->
-	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
+      | Default k ->
+	  let (loc,na) = List.hd nal in
+	    (* TODO: fail if several names with different implicit types *)
+	  let ty = locate_if_isevar loc na (intern_type env ty) in
+	    List.fold_left
+	      (fun ((ids,unb,ts,sc),bl) (_,na) ->
+		((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
+	      (env,bl) nal
+      | Generalized (b,b',t) ->
+	  intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty)
   | LocalRawDef((loc,na),def) ->
-      ((name_fold Idset.add na ids,ts,sc),
+      ((name_fold Idset.add na ids,unb,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
 (**********************************************************************)
@@ -794,7 +804,7 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalise sigma globalenv env allow_patvar lvar c =
-  let rec intern (ids,tmp_scope,scopes as env) = function
+  let rec intern (ids,unb,tmp_scope,scopes as env) = function
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env lvar [] ref in
@@ -818,17 +828,17 @@ let internalise sigma globalenv env allow_patvar lvar c =
 		   | None -> 0
 	       in
 	       let before, after = list_chop idx bl in
-	       let ((ids',_,_) as env',rbefore) =
+	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
 	       let ro =
 		 match c with 
 		   | None -> RStructRec 
-		   | Some c' -> f (intern (ids', tmp_scope, scopes) c') 
+		   | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c') 
 	       in 
 	       let n' = Option.map (fun _ -> List.length before) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
-	     let n, ro, ((ids',_,_),rbl) =
+	     let n, ro, ((ids',_,_,_),rbl) =
 	       (match order with
 		 | CStructRec -> 
 		     intern_ro_arg None (fun _ -> RStructRec)
@@ -839,8 +849,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	     in
 	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
-             intern_type (ids',tmp_scope,scopes) ty,
-             intern (ids'',None,scopes) bd)) dl in
+             intern_type (ids',unb,tmp_scope,scopes) ty,
+             intern (ids'',unb,None,scopes) bd)) dl in
 	RRec (loc,RFix 
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
@@ -857,12 +867,12 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	in
         let idl = Array.map
           (fun (id,bl,ty,bd) ->
-            let ((ids',_,_),rbl) =
+            let ((ids',_,_,_),rbl) =
               List.fold_left intern_local_binder (env,[]) bl in
 	    let ids'' = List.fold_right Idset.add lf ids' in
             (List.rev rbl,
-             intern_type (ids',tmp_scope,scopes) ty,
-             intern (ids'',None,scopes) bd)) dl in
+             intern_type (ids',unb,tmp_scope,scopes) ty,
+             intern (ids'',unb,None,scopes) bd)) dl in
 	RRec (loc,RCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
@@ -892,7 +902,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	Dumpglob.dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
-	intern (ids,None,find_delimiters_scope loc key::scopes) e
+	intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
@@ -980,7 +990,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     (ids,List.flatten mpl')
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
-  and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
+  and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
@@ -988,16 +998,16 @@ let internalise sigma globalenv env allow_patvar lvar c =
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       List.iter message_redundant_alias asubst;
-      let rhs' = intern (env_ids,tmp_scope,scopes) rhs in
+      let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
-  and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
+  and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
     let tm' = intern env tm in
     let ids,typ = match t with
     | Some t -> 
 	let tids = ids_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
-	let t = intern_type (tids,None,scopes) t in
+	let t = intern_type (tids,unb,None,scopes) t in
 	let loc,ind,l = match t with
 	    | RRef (loc,IndRef ind) -> (loc,ind,[])
 	    | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
@@ -1033,9 +1043,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     in
       match bk with
 	| Default b -> default env b nal
-	| TypeClass (b,b') -> 
-	    let env, ibind = intern_typeclass_binder intern_type lvar
-	      (env, []) (List.hd nal,(b,b'),ty) in
+	| Generalized (b,b',t) -> 
+	    let env, ibind = intern_generalized_binder intern_type lvar
+	      env [] (List.hd nal) b b' t ty in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1049,9 +1059,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass (b, b') ->	  
-	  let env, ibind = intern_typeclass_binder intern_type lvar
-	    (env, []) (List.hd nal,(b,b'),ty) in
+      | Generalized (b, b', t) ->	  
+	  let env, ibind = intern_generalized_binder intern_type lvar
+	    env [] (List.hd nal) b b' t ty in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
@@ -1117,7 +1127,7 @@ let intern_gen isarity sigma env
                c =
   let tmp_scope = 
     if isarity then Some Notation.type_scope else None in
-    internalise sigma env (extract_ids env, tmp_scope,[])
+    internalise sigma env (extract_ids env, false, tmp_scope,[])
       allow_patvar (ltacvars,Environ.named_context env, [], impls) c
       
 let intern_constr sigma env c = intern_gen false sigma env c 
@@ -1206,7 +1216,7 @@ let interp_aconstr impls (vars,varslist) a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
-  let c = internalise Evd.empty (Global.env()) (extract_ids env, None, [])
+  let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
     false (([],[]),Environ.named_context env,vl,([],impls)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
@@ -1240,7 +1250,7 @@ let intern_context sigma env params =
   let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
     snd (List.fold_left
 	    (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
-	    ((extract_ids env,None,[]), []) params)
+	    ((extract_ids env,false,None,[]), []) params)
 
 let interp_context_gen understand_type understand_judgment env bl = 
   let (env, par, _, impls) =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7801f048fe..f726f8992e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -63,6 +63,72 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
 
+let add_name_to_ids set na = 
+  match na with 
+  | Anonymous -> set 
+  | Name id -> Idset.add id set 
+	
+let free_vars_of_rawconstr ?(bound=Idset.empty) =
+  let rec vars bound vs = function
+    | RVar (loc,id) -> 
+	if is_freevar bound (Global.env ()) id then
+	  if List.mem_assoc id vs then vs 
+	  else (id, loc) :: vs
+	else vs
+    | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
+    | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> 
+	let vs' = vars bound vs ty in 
+	let bound' = add_name_to_ids bound na in 
+	vars bound' vs' c
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
+	let vs1 = vars_option bound vs rtntypopt in 
+	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in 
+	List.fold_left (vars_pattern bound) vs2 pl
+    | RLetTuple (loc,nal,rtntyp,b,c) ->
+	let vs1 = vars_return_type bound vs rtntyp in 
+	let vs2 = vars bound vs1 b in 
+	let bound' = List.fold_left add_name_to_ids bound nal in
+	vars bound' vs2 c
+    | RIf (loc,c,rtntyp,b1,b2) -> 
+	let vs1 = vars_return_type bound vs rtntyp in 
+	let vs2 = vars bound vs1 c in 
+	let vs3 = vars bound vs2 b1 in 
+	vars bound vs3 b2
+    | RRec (loc,fk,idl,bl,tyl,bv) ->
+	let bound' = Array.fold_right Idset.add idl bound in 
+	let vars_fix i vs fid = 
+	  let vs1,bound1 = 
+	    List.fold_left 
+	      (fun (vs,bound) (na,k,bbd,bty) -> 
+		 let vs' = vars_option bound vs bbd in 
+		 let vs'' = vars bound vs' bty in
+		 let bound' = add_name_to_ids bound na in 
+		 (vs'',bound')
+	      )
+	      (vs,bound')
+	      bl.(i)
+	  in
+	  let vs2 = vars bound1 vs1 tyl.(i) in 
+	  vars bound1 vs2 bv.(i)
+	in
+	array_fold_left_i vars_fix vs idl
+    | RCast (loc,c,k) -> let v = vars bound vs c in 
+	(match k with CastConv (_,t) -> vars bound v t | _ -> v)
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
+
+  and vars_pattern bound vs (loc,idl,p,c) = 
+    let bound' = List.fold_right Idset.add idl bound  in 
+    vars bound' vs c
+
+  and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
+
+  and vars_return_type bound vs (na,tyopt) = 
+    let bound' = add_name_to_ids bound na in 
+    vars_option bound' vs tyopt
+  in 
+  fun rt -> List.rev (vars bound [] rt)
+      
+
 let ids_of_names l = 
   List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
 
@@ -138,14 +204,10 @@ let combine_params_freevar avoid applied needed =
 	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
     applied needed
 
-let compute_context_vars env l =
-  List.fold_left (fun avoid (iid, _, c) -> 
-    (match snd iid with Name i -> [i] | Anonymous -> []) @ (free_vars_of_constr_expr c ~bound:env avoid))
-    [] l
-
 let destClassApp cl =
   match cl with
     | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+    | CAppExpl (loc, (None, ref), l) -> loc, ref, l
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
       
@@ -155,92 +217,19 @@ let destClassAppExpl cl =
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
-let full_class_binders env l = 
-  let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
-  let l', avoid =
-    List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
-      match bk with
-	  Implicit -> 
-	    let (loc, id, l) = 
-	      try destClassAppExpl cl 
-	      with Not_found -> 
-		user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
-	    in
-	    let gr = Nametab.global id in
-	      (try
-		  let c = class_info gr in
-		  let (ci, rd) = c.cl_context in
-		  let pars = List.rev (List.combine ci rd) in
-		  let args, avoid = combine_params_freevar avoid l pars in
-		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
-		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
-	| Explicit -> (x :: l', avoid))
-      ([], avoid) l
-  in List.rev l'
-
-let compute_context_freevars env ctx =
-  let bound, ids = 
-    List.fold_left 
-      (fun (bound, acc) (oid, id, x) -> 
-	let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in
-	  bound, free_vars_of_constr_expr x ~bound acc)
-      (env,[]) ctx
-  in freevars_of_ids env (List.rev ids)
-
-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, None)) elts
+let full_class_binder env (loc, id, l) gr = 
+  let avoid = 
+    Idset.union env (ids_of_list 
+			(free_vars_of_constr_expr (CApp (loc, (None, mkRefC id), l)) ~bound:env []))
   in
-    fv_ctx, ctx
-
-let full_class_binder env (iid, (bk, bk'), cl as c) = 
-  let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in
   let c, avoid =
-    match bk' with
-    | Implicit -> 
-	let (loc, id, l) = 
-	  try destClassAppExpl cl 
-	  with Not_found -> 
-	    user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
-	in
-	let gr = Nametab.global id in
-	  (try
-	      let c = class_info gr in
-	      let (ci, rd) = c.cl_context in
-	      let pars = List.rev (List.combine ci rd) in
-	      let args, avoid = combine_params_freevar avoid l pars in
-		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
-	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
-    | Explicit -> ((iid,bk,cl), avoid)
+    let c = class_info gr in
+    let (ci, rd) = c.cl_context in
+    let pars = List.rev (List.combine ci rd) in
+    let args, avoid = combine_params_freevar avoid l pars in
+      CAppExpl (loc, (None, id), args), avoid
   in c
 
-let compute_constraint_freevars env (oid, _, x) =
-  let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in
-  let ids = free_vars_of_constr_expr x ~bound [] in
-    freevars_of_ids env (List.rev ids)
-
-let resolve_class_binder env c = 
-  let cstr = full_class_binder env c in
-  let fv_ctx = 
-    let elts = compute_constraint_freevars env cstr in
-      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
-  in fv_ctx, cstr
-    
-let generalize_class_binder_raw env c = 
-  let env = Idset.union env (Termops.vars_of_env (Global.env())) in
-  let fv_ctx, cstr = resolve_class_binder env c in
-  let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in
-  let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in
-    ids', ctx', cstr
-
-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 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 ac1b8c99a7..744b45272f 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -32,6 +32,8 @@ val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
   Names.identifier list -> Names.identifier list
 
+val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+
 val binder_list_of_ids : identifier list -> local_binder list
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
@@ -39,17 +41,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 resolve_class_binders : Idset.t -> typeclass_context -> 
-  (identifier located * constr_expr) list * typeclass_context
-
-val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
-
-val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> 
-  Idset.t * typeclass_context * typeclass_constraint
-  
-val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
-  (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
-
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params : Names.Idset.t ->
@@ -59,3 +50,6 @@ val combine_params : Names.Idset.t ->
   ((global_reference * bool) option * Term.rel_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
+val full_class_binder : Idset.t -> 
+  loc * reference * (constr_expr * explicitation located option) list ->
+  global_reference -> constr_expr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 058d997e0d..935d95fc54 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -502,9 +502,12 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
 	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
-      let sigma = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+      let sigma = 
+	try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' 
+	with Option.Heterogeneous -> raise No_match 
+      in
       let sigma = List.fold_left2 
-       (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
+      (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
       List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
   | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) 
       when List.length nal1 = List.length nal2 ->
@@ -603,7 +606,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
 
-type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
+type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index eb166bc254..b2d74beed2 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -98,7 +98,11 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
   
-type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
+type binder_kind = 
+  | Default of binding_kind 
+  | Generalized of binding_kind * binding_kind * bool
+      (* Inner binding, outer bindings, typeclass-specific flag
+	 for implicit generalization of superclasses *)
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)