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. --- vernac/vernacentries.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/vernacentries.mli') diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 3c88a3443..02a3b2bd6 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,11 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit +val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit (** Vernacular entries *) val vernac_require : - Libnames.reference option -> bool option -> Libnames.reference list -> unit + Libnames.qualid option -> bool option -> Libnames.qualid list -> unit (** The main interpretation function of vernacular expressions *) val interp : -- cgit v1.2.3