diff options
| author | Gregory Malecha | 2013-12-12 14:53:00 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2013-12-12 14:53:26 +0100 |
| commit | b4ed8ee3ad7fffe5594df17b0b343e649fc44d1e (patch) | |
| tree | 567fd29c2fb3c5103b8942addb12f2938f07aed3 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 567bde9cac..54f8310103 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 -> |