| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-05-12 | Extraction: fix the detection of the "polyprop" situation | Pierre Letouzey | |
| The ~polyprop argument wasn't propagated properly anymore, leading the extraction to try to operate on situations it cannot handle (yet). Cf Table.error_singleton_become_prop for more details. Regression test added. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |