Generalized implementation of generalization.

- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.


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

16 files changed, 145 insertions, 161 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 027aae7a7..46e33360c 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -613,6 +613,7 @@ let rec add_args id new_args b =
   | CCast(loc,b1,CastCoerce) ->
       CCast(loc,add_args id new_args b1,CastCoerce)
   | CNotation _ -> anomaly "add_args : CNotation"
+  | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
   | CDynamic _ -> anomaly "add_args : CDynamic"
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 561ed3d4c..4e910935a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -396,6 +396,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
    | CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
+   | CGeneralization(_,_,_,_) -> xlate_error "CGeneralization: TODO"
    | CPrim (_, Numeral i) -> 
        CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
    | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 56bd40d30..7b8d982d1 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -92,45 +92,27 @@ 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 ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri =
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) 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
-      | Implicit ->
-	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = class_info (Nametab.global id) in
-	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in
-	    if needlen <> applen then 
-	      Classes.mismatched_params env (List.map fst par) (snd k.cl_context);
-	    let (ci, rd) = k.cl_context in
-	    let pars = List.rev (List.combine ci rd) in
-	    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 pars
-	    in Topconstr.CAppExpl (loc, (None, id), pars)
-
+    | Implicit ->
+	Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
+	  ~allow_partial:false (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)
+		  else CHole (Util.dummy_loc, None)
+		in t, avoid
+	    | None -> failwith ("new instance: under-applied typeclass"))
+	  cl
       | Explicit -> 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
-  on_free_vars (List.rev (gen_ids @ fvs));
-  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.append ctx (List.rev gen_ctx) in
+  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   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
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index f2522589f..583c1a165 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -37,6 +37,6 @@ val new_instance :
   Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
-  ?on_free_vars:(identifier list -> unit) ->
+  ?generalize:bool ->
   int option ->
   identifier * Subtac_obligations.progress
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9b8f62aa0..cfa88f3cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -696,17 +696,8 @@ let push_loc_name_env lvar (ids,unb,tmpsc,scopes as env) loc = function
 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
+      Implicit_quantifiers.implicit_application ids
+	Implicit_quantifiers.combine_params_freevar ty
   in
   let ty = intern_type (ids,true,tmpsc,sc) ty in
   let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty in
@@ -731,6 +722,30 @@ let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl)
       ((name_fold Idset.add na ids,unb,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
+let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
+  let c = intern (ids,true,tmp_scope,scopes) c in
+  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
+  let env', c' = 
+    let abs = 
+      let pi = 
+	match ak with
+	| Some AbsPi -> true
+	| None when tmp_scope = Some Notation.type_scope 
+	    || List.mem Notation.type_scope scopes -> true
+	| _ -> false
+      in 
+	if pi then
+	  (fun (id, loc') acc ->
+	    RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+	else
+	  (fun (id, loc') acc -> 
+	    RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+    in
+      List.fold_right (fun (id, loc as lid) (env, acc) -> 
+	let env' = push_loc_name_env lvar env loc (Name id) in
+	  (env', abs lid acc)) fvs (env,c) 
+  in c'
+
 (**********************************************************************)
 (* Utilities for application                                          *)
 
@@ -897,6 +912,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CNotation (_,"( _ )",([a],[])) -> intern env a
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
+    | CGeneralization (loc,b,a,c) ->
+        intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
 	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
 	Dumpglob.dump_notation_location (fst (unloc loc)) df;
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4daf21955..876af8f54 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -200,14 +200,12 @@ let combine_params avoid fn applied needed =
       | (x,_) :: _, [] -> 
 	  user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
-    
-let combine_params_freevar avoid applied needed =
-  combine_params avoid
-    (fun avoid (_, (na, _, _)) -> 
-      let id' = next_name_away_from na avoid in
-	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
-    applied needed
 
+let combine_params_freevar =
+  fun avoid (_, (na, _, _)) -> 
+    let id' = next_name_away_from na avoid in
+      (CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
+	
 let destClassApp cl =
   match cl with
     | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
@@ -221,19 +219,34 @@ let destClassAppExpl cl =
     | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
-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
-  let c, 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 implicit_application env ?(allow_partial=true) f ty = 
+  let is_class =
+    try
+      let (loc, r, _ as clapp) = 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 ((loc, id, par), gr) -> 
+	let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+	let c, avoid =
+	  let c = class_info gr in
+	  let (ci, rd) = c.cl_context in
+	  if not allow_partial then
+	    begin 
+	      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 -> if x = None then succ acc else acc) 0 ci in
+		if needlen <> applen then 
+		  Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+	    end;
+	  let pars = List.rev (List.combine ci rd) in
+	  let args, avoid = combine_params avoid f par pars in
+	    CAppExpl (loc, (None, id), args), avoid
+	in c
+	  
 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 744b45272..593427209 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -43,13 +43,11 @@ val free_vars_of_binders :
 
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
-val combine_params : Names.Idset.t ->
+val combine_params_freevar :
+  Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+  Topconstr.constr_expr * Names.Idset.t
+
+val implicit_application : Idset.t -> ?allow_partial:bool ->
   (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.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
+  constr_expr -> constr_expr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 935d95fc5..c0b81c90c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -608,6 +608,8 @@ type explicitation = ExplByPos of int * identifier option | ExplByName of identi
 
 type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool
 
+type abstraction_kind = AbsLambda | AbsPi
+
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
@@ -648,6 +650,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr notation_substitution
+  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
@@ -715,6 +718,7 @@ let constr_loc = function
   | CSort (loc,_) -> loc
   | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
+  | CGeneralization (loc,_,_,_) -> loc
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
   | CDynamic _ -> dummy_loc
@@ -798,6 +802,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
+  | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
       acc
@@ -910,6 +915,7 @@ let map_constr_expr_with_binders g f e = function
   | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
   | CNotation (loc,n,(l,ll)) ->
       CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
+  | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CPrim _ | CDynamic _ | CRef _ as x -> x
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b2d74beed..0064d238d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -104,6 +104,8 @@ type binder_kind =
       (* Inner binding, outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
+type abstraction_kind = AbsLambda | AbsPi
+
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
@@ -144,6 +146,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr notation_substitution
+  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5f729762f..77b4f003c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -24,7 +24,8 @@ open Util
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
+    "Prop"; "Set"; "Type"; ".("; "_"; "..";
+    "`{"; "`("; ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 
@@ -203,7 +204,12 @@ GEXTEND Gram
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",([c],[]))
-            | _ -> c) ] ]
+            | _ -> c)
+      | "`{"; c = operconstr LEVEL "200"; "}" ->
+	  CGeneralization (loc, Implicit, None, c)
+      | "`("; c = operconstr LEVEL "200"; ")" ->
+	  CGeneralization (loc, Explicit, None, c)
+      ] ]
   ;
   forall: 
     [ [ "forall" -> () 
@@ -400,8 +406,12 @@ GEXTEND Gram
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
     | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc
+    | "{"; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; "}" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
     | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+    | "("; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; ")" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Implicit, b), t)) tc
     | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 239d3772f..a2cad8e17 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -92,6 +92,14 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
+let pr_generalization bk ak c =
+  let hd, tl =
+    match bk with 
+    | Implicit -> "{", "}"
+    | Explicit -> "(", ")"
+  in (* TODO: syntax Abstraction Kind *) 
+    str "`" ++ str hd ++ c ++ str tl
+
 let pr_com_at n =
   if Flags.do_translate() && n <> 0 then comment n 
   else mt()
@@ -597,6 +605,7 @@ let rec pr sep inherited a =
   | CNotation (_,"( _ )",([t],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
+  | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
   | CDynamic _ -> str "<dynamic>", latom
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 662f2ac58..1ae1196a3 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1243,9 +1243,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance binders instance fields = 
-  new_instance binders instance fields 
-    ~on_free_vars:Classes.fail_on_free_vars
-    None
+  new_instance binders instance fields ~generalize:false None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1524,8 +1522,7 @@ let add_morphism binders m s n =
   in	  
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance binders instance []
-	      ~on_free_vars:Classes.fail_on_free_vars
-	      ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
 	      None)
 
 VERNAC COMMAND EXTEND AddSetoid1
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
new file mode 100644
index 000000000..d86d34d35
--- /dev/null
+++ b/test-suite/success/Generalization.v
@@ -0,0 +1,13 @@
+
+Check `(a = 0).
+Check `(a = 0)%type.
+Definition relation A := A -> A -> Prop.
+Definition equivalence {(R : relation A)} := True.
+Check (`(@equivalence A R)).
+
+Definition a_eq_b : `( a = 0 /\ a = b /\ b > c \/ d = e /\ d = 1).
+Admitted.
+Print a_eq_b.
+
+
+
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b58998d1f..d286b190f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -93,21 +93,12 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
    : Irreflexive (complement R).
 
   Next Obligation. 
-  Proof. 
-    unfold complement.
-    red. intros H.
-    intros H' ; apply H'.
-    apply reflexivity.
-  Qed.
-
+  Proof. firstorder. Qed.
 
 Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
 
   Next Obligation.
-  Proof.
-    red ; intros H'.
-    apply (H (symmetry H')).
-  Qed.
+  Proof. firstorder. Qed.
 
 (** * Standard instances. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 301f9bf2a..4e8710918 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -270,17 +270,6 @@ let type_ctx_instance isevars env ctx inst subst =
       (subst, []) (List.rev ctx) inst
   in s
 
-(* let type_ctx_instance isevars env ctx inst subst = *)
-(*   let (s, _, _) =  *)
-(*     List.fold_left2 *)
-(*       (fun (s, env, n) (na, _, t) ce -> *)
-(* 	let t' = substnl subst n t in *)
-(* 	let c = interp_casted_constr_evars isevars env ce t' in *)
-(* 	let d = na, Some c, t' in *)
-(* 	  (substl s c :: s, push_rel d env, succ n)) *)
-(*       ([], env, 0) (List.rev ctx) inst *)
-(*   in s @ subst *)
-
 let refine_ref = ref (fun _ -> assert(false))
 
 let id_of_class cl =
@@ -294,23 +283,6 @@ let id_of_class cl =
 open Pp
 
 let ($$) g f = fun x -> g (f x)
-
-let default_on_free_vars =
-  Flags.if_verbose
-    (fun fvs ->
-      match fvs with
-	  [] -> ()
-	| l -> msgnl (str"Implicitly generalizing " ++ 
-			 prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str"."))
-
-let fail_on_free_vars = function
-    [] -> ()
-  | [fv] ->
-      errorlabstrm "Classes" 
-	(str"Unbound variable " ++ Nameops.pr_id fv ++ str".")
-  | fvs -> errorlabstrm "Classes" 
-      (str"Unbound variables " ++
-	  prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".")
 	
 let instance_hook k pri global imps ?hook cst = 
   let inst = Typeclasses.new_instance k pri global cst in
@@ -333,47 +305,24 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     instance_hook k pri global imps ?hook kn;
     id
 
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) 
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) 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
-      | Implicit ->
-	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = class_info (Nametab.global id) in
-	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in
-	    if needlen <> applen then 
-	      mismatched_params env (List.map fst par) (snd k.cl_context);
-	    let (ci, rd) = k.cl_context in
-	    let pars = List.rev (List.combine ci rd) in
-	    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.ImplicitArg (k.cl_impl, (1, None))))
-			else CHole (Util.dummy_loc, None)
-		      in t, avoid
-		  | None -> failwith ("new instance: under-applied typeclass"))
-	      par pars
-	    in Topconstr.CAppExpl (loc, (None, id), pars)
-
-      | Explicit -> cl
+    | Implicit ->
+	Implicit_quantifiers.implicit_application Idset.empty
+	  (fun avoid (clname, (id, _, t)) -> 
+	    match clname with 
+	    | Some (cl, b) -> 
+		let t = CHole (Util.dummy_loc, None) in
+		  t, avoid
+	    | None -> failwith ("new instance: under-applied typeclass"))
+	  cl
+    | Explicit -> 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
-  on_free_vars (List.rev fvs @ List.rev gen_ids);
-  let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in
-  let bound = Idset.union gen_idset ctx_bound in
-  let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
-  let ctx, avoid = name_typeclass_binders bound ctx in
-  let ctx = List.append ctx (List.rev gen_ctx) in
+  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let imps, c' = interp_type_evars isevars env c in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 970f3e2ab..4f20f1649 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -47,12 +47,6 @@ val new_class : identifier located ->
   local_binder list ->
   binder_list -> unit
 
-(* By default, print the free variables that are implicitely generalized. *)
-
-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
@@ -73,7 +67,7 @@ val new_instance :
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
-  ?on_free_vars:(identifier list -> unit) ->
+  ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
   ?hook:(constant -> unit) ->
   int option ->