| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Using name given by user to name a 'pat, if any. |  Hugo Herbelin | 2018-02-20 |
| | | | | | This works for contexts in Definition and co, but not yet for "fun" and co. | ||
| * | A test checking for non-collision of name in irrefutable patterns. | Hugo Herbelin | 2017-03-23 |
| | | |||
| * | Updating a comment in test-suite. | Hugo Herbelin | 2016-11-10 |
| | | |||
| * | Fixing output test-suite after warning for inner Requires. |  Pierre-Marie Pédrot | 2016-08-30 |
| | | |||
| * | Some extra fixes in printing patterns in binders. | Hugo Herbelin | 2016-07-19 |
| | | | | | | | | | | | - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me. | ||
| * | Patterns in binders: printing tests |  Arnaud Spiwack | 2016-06-27 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |