diff options
| author | msozeau | 2008-04-12 16:08:04 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-12 16:08:04 +0000 |
| commit | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch) | |
| tree | ff43de2111efb4a9b9db28e137130b4d7854ec69 /contrib | |
| 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 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 5 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.mli | 1 |
2 files changed, 4 insertions, 2 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 |