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 /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions