diff options
author | 2008-04-12 16:08:04 +0000 | |
---|---|---|
committer | 2008-04-12 16:08:04 +0000 | |
commit | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch) | |
tree | ff43de2111efb4a9b9db28e137130b4d7854ec69 /toplevel/classes.ml | |
parent | 1ea4a8d26516af14670cc677a5a0fce04b90caf7 (diff) |
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
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r-- | toplevel/classes.ml | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index a539a87ba..db87d36ab 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 |