| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-06 | Remove old overlays | Gaëtan Gilbert | |
| I updated the readme example using the most recent overlay with only 1 touched development. | |||
| 2019-02-28 | Constructor type information uses the expanded form. | Pierre-Marie Pédrot | |
| It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |