diff options
| author | Hugo Herbelin | 2017-04-13 12:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-13 12:31:02 +0200 |
| commit | 4e70791036a1ab189579e109b428f46f45698b59 (patch) | |
| tree | 4b3deb27bccb52fdafe19a75e065cbf1aec2d299 /kernel/type_errors.ml | |
| 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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions