From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 13 Jun 2018 00:22:57 +0200 Subject: Remove reference name type. 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. --- dev/doc/changes.md | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dev/doc') diff --git a/dev/doc/changes.md b/dev/doc/changes.md index bb8189efc..f3fc126f9 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,14 @@ ### ML API +Names + +- In `Libnames`, the type `reference` and its two constructors `Qualid` and + `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, + `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be + replaced by a test using `qualid_is_ident`. Extracting the ident part of a + qualid can be done using `qualid_basename`. + Misctypes - Syntax for universe sorts and kinds has been moved from `Misctypes` -- cgit v1.2.3