| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-09-02 | Fixes #9403 and #10803 (missing flattening of nested applications in notations). | Hugo Herbelin | |
| The bugs involved: - a notation with a subterm in position of function of an application - use of this notation in another notation creating a non-flattened application In particular, this fooled "find_appl_head" (for #10803) and the translation from GApp to NApp (for #9403). We fix the translation NApp -> GApp (since glob_constr is supposed to have its applications flattened). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |