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

2 files changed, 30 insertions, 3 deletions

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 ->