| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-13 | Fixes #13363: case of a meta not paying attention to being under binders. | Hugo Herbelin | |
| In Evar := C[Meta] problems of unification.ml, and C[ ] contains binders, Meta was wrongly considered by pose_all_metas_as_evars as under these binders (while Metas are always defined in the initial context of the unification problem). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |