| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Using fold_glob_constr_with_binders to code bound_glob_vars. |  Hugo Herbelin | 2017-04-13 |
| | | | | | | | | | | 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. | ||
| * | Adding a fold_glob_constr_with_binders combinator. | Hugo Herbelin | 2017-04-13 |
| 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". | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |