diff options
| author |  Gregory Malecha <gmalecha@eecs.harvard.edu> | 2013-12-12 14:53:00 +0100 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-12 14:53:26 +0100 |
| commit | b4ed8ee3ad7fffe5594df17b0b343e649fc44d1e (patch) | |
| tree | 567fd29c2fb3c5103b8942addb12f2938f07aed3 /library/libnames.mli | |
| parent | d6c7bf2ec750876c9b35ee9d84840f2ab643dbfe (diff) | |
Patch for supporting [From Xxx Require Yyy Zzz.]
When using libraries I find it convenient (and future proof) to use fully qualified paths in many places. It would be nice to have a convenient short-hand for this so that you can:
From Xxx Require Yyy Zzz.
instead of having to type:
Require Xxx.Yyy Xxx.Zzz.
Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
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 *) |