diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /vernac/vernacentries.mli | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
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.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 : |