diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 60ec7af79..9a5fa8be4 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -124,6 +124,7 @@ val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> Loc.t +val join_reference : reference -> reference -> reference (** Deprecated synonyms *) |