| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"." |  Maxime Dénès | 2017-04-28 |
| * | Using a more explicit algebraic type for evars of kind "MatchingVar". |  Hugo Herbelin | 2017-04-28 |
| * | Adding a new evar source to remember the name of evars which were | Hugo Herbelin | 2017-01-22 |
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | Tentatively more informative report of failure when inferring | Hugo Herbelin | 2014-12-11 |
| * | Improved tracking of the origin of evars. | Hugo Herbelin | 2014-12-07 |
| * | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin | 2014-06-13 |
| * | Modulification of name |  ppedrot | 2012-12-18 |
| * | Modulification of identifier | ppedrot | 2012-12-14 |
| * | Updating headers. |  herbelin | 2012-08-08 |
| * | global_reference migrated from Libnames to new Globnames, less deps in gramma... |  letouzey | 2012-05-29 |
| * | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |