| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-20 | Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars). | Hugo Herbelin | |
| We fix it by reducing K-redexes the same in the both places (make_tuple and minimal_free_rels) which compute the dependencies of a dependent equality. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |