| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Remove reference name type. |  Maxime Dénès | 2018-06-18 |
| | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. | ||
| * | [api] Misctypes removal: miscellaneous aliases. |  Emilio Jesus Gallego Arias | 2018-06-12 |
| | | |||
| * | Split off Universes functions dealing with names. |  Gaëtan Gilbert | 2018-05-17 |
| This API is a bit strange, I expect it will change at some point. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |