Add the ability to specify what to do with free variables in instance

declarations. By default, print the list of implicitely generalized
variables. Implement new commands Add Parametric Relation/Morphism for...
parametric relations and morphisms. Now the Add * commands are strict
about free vars and will fail if there remain some. Parametric just allows to
give a variable context. Also, correct a bug in generalization of
implicits that ordered the variables in the wrong order.


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

11 files changed, 224 insertions, 134 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 4b4a6458b9..cb3873bdfb 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -100,7 +100,7 @@ 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 ctx (instid, bk, cl) props pri =
+let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) 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
@@ -133,9 +133,10 @@ let new_instance ctx (instid, bk, cl) props pri =
   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.rev_append gen_ctx ctx in
+  let ctx = List.append ctx (List.rev gen_ctx) 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 9a6730454a..92a94cda65 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -36,5 +36,6 @@ val new_instance :
   Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  ?on_free_vars:(identifier list -> unit) ->
   int option ->
   identifier
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 2610f10368..cf37efc77a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -71,12 +71,12 @@ 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
+	let l' = 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
+	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
 	
     | [] -> bdvars, l
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f00515ab6c..9b0bb188b9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -550,8 +550,8 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
 	    new_evar isevars env relty
       | Some x -> f x
   in
-  let rec aux t l =
-    let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) t in
+  let rec aux ty l =
+    let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
     match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
 	  let (b, arg, evars) = aux b cstrs in
@@ -563,7 +563,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota t in
+		let t = Reductionops.nf_betaiota ty in
 		let rel = mk_relty t None in 
 		  t, rel, [t, rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
@@ -680,7 +680,7 @@ let rewrite2_unif_flags = {
 (* let unification_rewrite c1 c2 cl but gl =  *)
 (*   let (env',c1) = *)
 (*     try *)
-(*       (\* ~flags:(false,true) to allow to mark occurences that must not be *)
+(*       (\* ~flags:(false,true) to allow to mark occurrences that must not be *)
 (*          rewritten simply by replacing them with let-defined definitions *)
 (*          in the context *\) *)
 (*       w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *)
@@ -989,10 +989,10 @@ open Genarg
 open Extraargs
 
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None ]
 | [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ]
 END
 
@@ -1084,25 +1084,31 @@ TACTIC EXTEND setoid_rewrite
    -> [ cl_rewrite_clause c o [] None ]
  | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] ->
       [ cl_rewrite_clause c o [] (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) ] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o occ None]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id)] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] ->
       [ cl_rewrite_clause c o occ (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ)] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] ->
       [ cl_rewrite_clause c o occ (Some (([],id), []))]
 END
 
 (* let solve_obligation lemma =  *)
 (*   tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *)
 (*     (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *)
-    
+
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
 
-let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit,
-				 CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
-					  [a;aeq]))
+let declare_an_instance n s args =
+  ((dummy_loc,Name n), Explicit,
+  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
+	   args))
 
-let anew_instance instance fields = new_instance [] instance fields None
+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
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1111,75 +1117,85 @@ let require_library dirpath =
 let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
-  if not (Library.library_is_opened dir) || not (Library.library_is_loaded dir) then
+  if (* not (Library.library_is_opened dir) ||  *)not (Library.library_is_loaded dir) then
     error ("Library "^(list_last d)^" has to be required first")
 
 let init_setoid () =
   check_required_library ["Coq";"Setoids";"Setoid"]
 
-let declare_instance_refl a aeq n lemma = 
+let declare_instance_refl binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" 
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
 
-let declare_instance_sym a aeq n lemma = 
+let declare_instance_sym binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric"
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "symmetry"),[],lemma)]
 
-let declare_instance_trans a aeq n lemma = 
+let declare_instance_trans binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" 
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
 
-let declare_relation a aeq n refl symm trans = 
+let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
   match (refl,symm,trans) with 
       (None, None, None) -> 
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" 
-	in ignore(anew_instance instance [])
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation"
+	in ignore(anew_instance binders instance [])
     | (Some lemma1, None, None) -> 
-	ignore (declare_instance_refl a aeq n lemma1)
+	ignore (declare_instance_refl binders a aeq n lemma1)
     | (None, Some lemma2, None) -> 
-	ignore (declare_instance_sym a aeq n lemma2)
+	ignore (declare_instance_sym binders a aeq n lemma2)
     | (None, None, Some lemma3) -> 
-	ignore (declare_instance_trans a aeq n lemma3)
+	ignore (declare_instance_trans binders a aeq n lemma3)
     | (Some lemma1, Some lemma2, None) -> 
-	ignore (declare_instance_refl a aeq n lemma1); 
-	ignore (declare_instance_sym a aeq n lemma2)
+	ignore (declare_instance_refl binders a aeq n lemma1); 
+	ignore (declare_instance_sym binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl a aeq n lemma1 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
-	    anew_instance instance 
+	    anew_instance binders instance 
 	      [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl);
 	       ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)])
     | (None, Some lemma2, Some lemma3) -> 
-	let lemma_sym = declare_instance_sym a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
-	    anew_instance instance 
+	    anew_instance binders instance 
 	      [((dummy_loc,id_of_string "per_sym"),  [], mkIdentC lemma_sym);
 	       ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)])
      | (Some lemma1, Some lemma2, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl a aeq n lemma1 in 
-	let lemma_sym = declare_instance_sym a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
+	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
-	    anew_instance instance 
-	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+	  anew_instance binders instance 
+	    [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+	     ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+	     ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+
+type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+
+let (wit_binders_let : Genarg.tlevel binders_let_argtype),
+  (globwit_binders_let : Genarg.glevel binders_let_argtype),
+  (rawwit_binders_let : Genarg.rlevel binders_let_argtype) =
+  Genarg.create_arg "binders_let"
+
+open Pcoq.Constr
 
 VERNAC COMMAND EXTEND AddRelation
-    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
+
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)  
 	"as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) None None ]
@@ -1208,6 +1224,40 @@ VERNAC COMMAND EXTEND AddRelation3
       [ declare_relation a aeq n None None (Some lemma3) ] 
 END
 
+VERNAC COMMAND EXTEND AddParametricRelation
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+	"reflexivity" "proved" "by" constr(lemma1) 
+	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+	"reflexivity" "proved" "by" constr(lemma1)  
+	"as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)  "as" ident(n) ] -> 
+      [ declare_relation ~binders:b a aeq n None None None ]
+END
+
+VERNAC COMMAND EXTEND AddParametricRelation2
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) 
+      "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
+END
+
+VERNAC COMMAND EXTEND AddParametricRelation3
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) 
+      "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] 
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+	"as" ident(n) ] ->  
+      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] 
+END
+
 let mk_qualid s =
   Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s)
 
@@ -1271,10 +1321,10 @@ let build_morphism_signature m =
     in aux t
   in
   let t', sig_, evars = build_signature isevars env t cstrs None snd in
-  let _ = List.iter 
+  let _ = List.iter
     (fun (ty, rel) -> 
       let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
-	ignore(Evarutil.e_new_evar isevars env default))
+	ignore (Evarutil.e_new_evar isevars env default))
     evars
   in
   let morph = 
@@ -1283,7 +1333,7 @@ let build_morphism_signature m =
   let evd = resolve_all_evars_once false (true, 15) env
     (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in
     Evarutil.nf_isevar evd morph
-
+	
 let default_morphism sign m =
   let env = Global.env () in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -1297,55 +1347,67 @@ let default_morphism sign m =
   let mor = resolve_one_typeclass env morph in
     mor, respect_projection mor morph
     	  
+let add_setoid binders a aeq t n =
+  init_setoid ();
+  let lemma_refl = declare_instance_refl binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
+  let lemma_sym = declare_instance_sym binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let lemma_trans = declare_instance_trans binders a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
+  let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
+  in ignore(
+    anew_instance binders instance
+      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+
+let add_morphism_infer m n =
+  init_setoid ();
+  let instance_id = add_suffix n "_Morphism" in
+  let instance = build_morphism_signature m in
+    if Lib.is_modtype () then 
+      let cst = Declare.declare_internal_constant instance_id
+	(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+      in
+	add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+	declare_projection n instance_id (ConstRef cst)
+    else
+      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	Flags.silently 
+	  (fun () ->
+	    Command.start_proof instance_id kind instance 
+	      (fun _ -> function
+		  Libnames.ConstRef cst -> 
+		    add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+		    declare_projection n instance_id (ConstRef cst)
+		| _ -> assert false);
+	    Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
+	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () 
+
+let add_morphism binders m s n =
+  init_setoid ();
+  let instance_id = add_suffix n "_Morphism" in
+  let instance = 
+    ((dummy_loc,Name instance_id), Explicit,
+    CAppExpl (dummy_loc, 
+	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
+	     [cHole; s; m]))
+  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))
+	      None)
+
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [	init_setoid ();
-	let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
-	let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-	let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
-	in ignore(
-	    anew_instance instance
-	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])]
+     [ add_setoid [] a aeq t n ]
+  | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     [	add_setoid binders a aeq t n ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ init_setoid ();
-	let instance_id = add_suffix n "_Morphism" in
-	let instance = build_morphism_signature m in
-	  if Lib.is_modtype () then 
-	    let cst = Declare.declare_internal_constant instance_id
-	      (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	    in
-	      add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
-	      declare_projection n instance_id (ConstRef cst)
-	  else
-	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	      Flags.silently 
-		(fun () ->
-		  Command.start_proof instance_id kind instance 
-		    (fun _ -> function
-			Libnames.ConstRef cst -> 
-			  add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
-			  declare_projection n instance_id (ConstRef cst)
-		      | _ -> assert false);
-		  Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
-	      Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () ]
-
+      [ add_morphism_infer m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ init_setoid ();
-	let instance_id = add_suffix n "_Morphism" in
-	let instance = 
-	  ((dummy_loc,Name instance_id), Explicit,
-	  CAppExpl (dummy_loc, 
-		   (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
-		   [cHole; s; m]))
-	in	  
-	let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-	  ignore(new_instance [] instance []
-		    ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
-		    None)
-      ]
+      [ add_morphism [] m s n ]
+  | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
+      [ add_morphism binders m s n ]
 END
 
 (** Bind to "rewrite" too *)
@@ -1375,7 +1437,7 @@ let check_evar_map_of_evars_defs evd =
 let unification_rewrite l2r c1 c2 cl rel but gl = 
   let (env',c') =
     try
-      (* ~flags:(false,true) to allow to mark occurences that must not be
+      (* ~flags:(false,true) to allow to mark occurrences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
       Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
@@ -1408,15 +1470,15 @@ let get_hyp gl c clause l2r =
 	
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
-let general_s_rewrite l2r c ~new_goals gl =
+let general_s_rewrite l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo = ref (get_hyp gl c None l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] None gl
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs None gl
 
-let general_s_rewrite_in id l2r c ~new_goals gl =
+let general_s_rewrite_in id l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo = ref (get_hyp gl c (Some id) l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] (Some (([],id), [])) gl
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs (Some (([],id), [])) gl
 
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 975dcf1dd0..552ff996ae 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -128,9 +128,9 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance [ subrelation A R R' ] => pointwise_subrelation :
+Instance [ sub : subrelation A R R' ] => pointwise_subrelation :
   subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
-Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed.
+Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
@@ -186,7 +186,7 @@ Program Instance [ Transitive A R ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -194,7 +194,7 @@ Program Instance [ Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -202,7 +202,7 @@ Program Instance [ Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
@@ -210,7 +210,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric _ R ] =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -218,7 +218,7 @@ Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ Equivalence A R ] (x : A) =>
+Program Instance [ Equivalence A R ] =>
   equivalence_partial_app_morphism : Morphism (R ==> iff) (R x).
 
   Next Obligation.
@@ -231,7 +231,7 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
+Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ]  =>
   Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
@@ -294,7 +294,7 @@ Program Instance inverse_iff_impl_id :
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
+Instance (A : Type) [ Reflexive B R ] =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
@@ -305,7 +305,7 @@ Proof. simpl_relation. Qed.
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
-  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). 
+  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
 Proof.
   reduce.
   unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
@@ -335,14 +335,14 @@ Qed.
 Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
-Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  inverse_respectful_norm : Normalizes _ (inverse R ==> inverse R') (inverse (R ==> R')) .
+Instance inverse_respectful_norm : 
+  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof. firstorder. Qed.
 
 (* If not an inverse on the left, do a double inverse. *)
 
-Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  not_inverse_respectful_norm : Normalizes _ (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+Instance not_inverse_respectful_norm : 
+  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
 Instance [ Normalizes B R' (inverse R'') ] =>
@@ -391,4 +391,3 @@ Ltac morphism_normalization :=
   end.
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
-
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f7f460123e..526264612f 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism x.
+  Reflexive_partial_app_morphism.
 
 Existing Instance setoid_partial_app_morphism.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 617ea6f4f6..e033343d1d 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -662,19 +662,19 @@ Add Relation key E.eq
 
 Implicit Arguments Equal [[elt]].
 
-Add Relation (t elt) Equal  
+Add Parametric Relation (elt : Type) : (t elt) Equal  
  reflexivity proved by (@Equal_refl elt)
  symmetry proved by (@Equal_sym elt)
  transitivity proved by (@Equal_trans elt)
  as EqualSetoid.
 
-Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
+Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
 unfold Equal; intros k k' Hk m m' Hm.
 rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@MapsTo elt)
+Add Parametric Morphism elt : (@MapsTo elt)
  with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
@@ -682,26 +682,26 @@ rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
  intuition.
 Qed.
 
-Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m.
+Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m.
 Proof.
 unfold Empty; intros m m' Hm; intuition.
 rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
+Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
+Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
+Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
 Proof.
 intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
@@ -712,7 +712,7 @@ rewrite <- H1, Hk, Hm, H2; auto.
 symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
-Add Morphism (@add elt) with signature 
+Add Parametric Morphism elt : (@add elt) with signature 
  E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
@@ -721,7 +721,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@remove elt) with signature
+Add Parametric Morphism elt : (@remove elt) with signature
  E.eq ==> Equal ==> Equal as remove_m.
 Proof.
 intros k k' Hk m m' Hm y.
@@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
+Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
+ Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index fc2cc81ebd..1a11f7a131 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd.
+Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index c063c7bc1d..f042ab0685 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -148,13 +148,13 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
 Qed.
 
-Add Relation (A -> B -> Prop) (@relations_eq A B)
+Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B)
   reflexivity proved by (proj1 (relations_eq_equiv A B))
   symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
   transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
 as relations_eq_rel.
 
-Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
+Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
 Proof.
 unfold relations_eq, well_founded; intros R1 R2 H;
 split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index a539a87baa..db87d36abf 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -412,7 +412,25 @@ open Pp
 
 let ($$) g f = fun x -> g (f x)
 
-let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
+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 new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) 
+    ?(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
@@ -444,10 +462,12 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho
   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 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.rev_append gen_ctx ctx in
+  let ctx = List.append ctx (List.rev gen_ctx) in
   let k, ctx', 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 c259971414..be0c98743e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -39,10 +39,17 @@ 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
+    
 val new_instance : 
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  ?on_free_vars:(identifier list -> unit) ->
   ?tac:Proof_type.tactic  ->
   ?hook:(constant -> unit) ->
   int option ->