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 /parsing/pcoq.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 'parsing/pcoq.mli')
-rw-r--r-- | parsing/pcoq.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9a45bc973..f959bd80c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,11 +213,11 @@ module Prim : val integer : int Gram.entry val string : string Gram.entry val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry + val reference : qualid Gram.entry + val qualid : qualid Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry + val smart_global : qualid or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry val ne_lstring : lstring Gram.entry @@ -232,7 +232,7 @@ module Constr : val binder_constr : constr_expr Gram.entry val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry - val global : reference Gram.entry + val global : qualid Gram.entry val universe_level : Glob_term.glob_level Gram.entry val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry |