| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-25 | Documenting syntax "injection ... as [= pat1 ... patn ]". | Hugo Herbelin | |
| To prevent confusion, forbidding a mix of the "injection term as pat1 ... patn" and of the "injection term as [= pat1 ... patn]" syntax: If a "[= ...]" occurs, this should be a singleton list of patterns. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |