diff options
| author | Hugo Herbelin | 2017-04-13 15:05:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-13 15:16:51 +0200 |
| commit | b4936da085b19ad508346d8e07ce1e922ef79c2d (patch) | |
| tree | 8a51b2bead7486af7f0a59efc6c4882f2d5cc087 /interp | |
| parent | 4e70791036a1ab189579e109b428f46f45698b59 (diff) | |
Using fold_glob_constr_with_binders to code bound_glob_vars.
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions