| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-12 | Fix #13330: Kernel messes with polymorphic side-effects. | Pierre-Marie Pédrot | |
| Polymorphic side-effects generated in monomorphic mode would be counted towards trusted subcomponents. This would allow to make ill-typed terms pass as legitimate by mimicking the shape of the inlining of monomorphic side-effects in such a proof. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |