| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-30 | Do not take universes into account in lia reification. | Pierre-Marie Pédrot | |
| This is slightly blunt, it might be the case that we get delayed constraints that cannot be solved resulting in a later universe inconsistency, but it looks highly unlikely on arithmetical statements. Alternatively we would have threaded the unification state, but this would have required a much deeper change. Fixes #9268. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |