Putting the From parameter of the Require command into the AST.

5 files changed, 26 insertions, 16 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 07891d0b48..450b1af0f9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -316,7 +316,7 @@ type vernac_expr =
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
-      export_flag option * lreference list
+      lreference option * export_flag option * lreference list
   | VernacImport of export_flag * lreference list
   | VernacCanonical of reference or_by_notation
   | VernacCoercion of obsolete_locality * reference or_by_notation *
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 70a8ec5522..cf7f6af28b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -465,11 +465,10 @@ GEXTEND Gram
 
       (* Requiring an already compiled module *)
       | IDENT "Require"; export = export_token; qidl = LIST1 global ->
-          VernacRequire (export, qidl)
+          VernacRequire (None, export, qidl)
       | 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)
+	VernacRequire (Some ns, export, qidl)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e0b94669c2..89ffae4b3e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -863,10 +863,14 @@ module Make
         | VernacNameSectionHypSet (id,set) ->
           return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
           str ":="++spc()++pr_using set))
-        | VernacRequire (exp, l) ->
+        | VernacRequire (from, exp, l) ->
+          let from = match from with
+          | None -> mt ()
+          | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+          in
           return (
             hov 2
-              (keyword "Require" ++ spc() ++ pr_require_token exp ++
+              (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
                  prlist_with_sep sep pr_module l)
           )
         | VernacImport (f,l) ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a0979f8b15..083fd54bfa 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -617,14 +617,17 @@ let rec tmpp v loc =
   | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
   | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
   | VernacNameSectionHypSet _ as x -> xmlTODO loc x
-  | VernacRequire (None,l) ->
-      xmlRequire loc (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some true,l) ->
-      xmlRequire loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some false,l) ->
-      xmlRequire loc ~attr:["import","true"] (List.map (fun ref ->
+  | VernacRequire (from, import, l) ->
+      let import = match import with
+      | None -> []
+      | Some true -> ["export","true"]
+      | Some false -> ["import","true"]
+      in
+      let from = match from with
+      | None -> []
+      | Some r -> ["from", Libnames.string_of_reference r]
+      in
+      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (true,l) ->
       xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4ffae0fff..62e5f0a324 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -749,7 +749,11 @@ let vernac_end_segment (_,id as lid) =
 
 (* Libraries *)
 
-let vernac_require import qidl =
+let vernac_require from import qidl =
+  let qidl = match from with
+  | None -> qidl
+  | Some ns -> List.map (Libnames.join_reference ns) qidl
+  in
   let qidl = List.map qualid_of_reference qidl in
   let modrefl = List.map Library.try_locate_qualified_library qidl in
   if Dumpglob.dump () then
@@ -1884,7 +1888,7 @@ let interp ?proof locality poly c =
 
   | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
 
-  | VernacRequire (export, qidl) -> vernac_require export qidl
+  | VernacRequire (from, export, qidl) -> vernac_require from export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
   | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t