| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-07-25 | Mark primitives integer as able to participate in reductions (fixes #10560). | Guillaume Melquiond | |
| The documentation states: - Norm means the term is fully normalized and cannot create a redex when substituted - Cstr means the term is in head normal form and that it can create a redex when substituted (i.e. constructor, fix, lambda) | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |