diff options
| -rw-r--r-- | library/libnames.ml | 24 | ||||
| -rw-r--r-- | library/libnames.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
3 files changed, 29 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 909a4dc3e..cf6d4c8ad 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -203,6 +203,30 @@ let eq_reference r1 r2 = match r1, r2 with | Ident (_, id1), Ident (_, id2) -> Id.equal id1 id2 | _ -> false +let join_reference ns r = + match ns , r with + Qualid (_, q1), Qualid (loc, q2) -> + let (dp1,id1) = repr_qualid q1 in + let (dp2,id2) = repr_qualid q2 in + Qualid (loc, + make_qualid + (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2) + id2) + | Qualid (_, q1), Ident (loc, id2) -> + let (dp1,id1) = repr_qualid q1 in + Qualid (loc, + make_qualid + (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) + id2) + | Ident (_, id1), Qualid (loc, q2) -> + let (dp2,id2) = repr_qualid q2 in + Qualid (loc, make_qualid + (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2) + id2) + | Ident (_, id1), Ident (loc, id2) -> + Qualid (loc, make_qualid + (dirpath_of_string (Names.Id.to_string id1)) id2) + (* Deprecated synonyms *) let make_short_qualid = qualid_of_ident 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 *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 567bde9ca..54f831010 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -439,6 +439,10 @@ GEXTEND Gram VernacRequire (export, qidl) | IDENT "Require"; export = export_token; filename = ne_string -> VernacRequireFrom (export, filename) + | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token + ; qidl = LIST1 global -> + let qidl = List.map (Libnames.join_reference ns) qidl in + VernacRequire (export, qidl) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr -> |