| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-04 | More extraction tests for inductive types with let-ins. | Hugo Herbelin | |
| 2021-04-04 | Fixing #13581: missing support for let-ins in arity of inductive types. | Hugo Herbelin | |
| At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |