| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixing #5460 (limitation in computing deps in pattern-matching compilation). |  Hugo Herbelin | 2017-04-08 |
| This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y |- match x, y, z with ... end". But still work to do for better management of dependencies in general... | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |