| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-22 | Ensure that a custom entry cannot be defined twice. | Pierre-Marie Pédrot | |
| This highlights the fact that diamond inheritance of a custom entry is a tricky problem, as well as merely importing two custom entries with the same name from two different modules. The only sane way to give a semantics to that is to stick to module-scoped objects, i.e. give those entries a kernel name. In the meantime, I went for a warning when overriding entries. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |