| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-25 | Use implicit arguments in notations for eq. | Gaëtan Gilbert | |
| This gives IMO slightly nicer errors when the type cannot be inferred, ie ~~~coq Type (forall x, x = x). ~~~ says "cannot infer the implicit parameter A of eq" instead of "cannot infer this placeholder". | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |