diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 12:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 12:31:02 +0200 |
| commit | 4e70791036a1ab189579e109b428f46f45698b59 (patch) | |
| tree | 4b3deb27bccb52fdafe19a75e065cbf1aec2d299 /pretyping/glob_ops.mli | |
| parent | 97f1d0b6ddfce894941d34fc3b3e4c4df0efadd2 (diff) | |
Adding a fold_glob_constr_with_binders combinator.
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533..af2834e49 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -37,6 +37,7 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list |