Forward compatibility with "From X Require Y."

1 files changed, 46 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
index c7a104b..37d737d 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
@@ -6021,6 +6021,52 @@ GEXTEND Gram
   ];
 END
 
+(* From *)
+let join_reference ns r =
+  Libnames.(
+  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 (string_of_id 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 (string_of_id id1)))
+	      id2)
+  | Ident (_, id1), Qualid (loc, q2) ->
+    let (dp2,id2) = repr_qualid q2 in
+    Qualid (loc, make_qualid
+      (append_dirpath (dirpath_of_string (string_of_id id1)) dp2)
+      id2)
+  | Ident (_, id1), Ident (loc, id2) ->
+    Qualid (loc, make_qualid
+      (dirpath_of_string (string_of_id id1)) id2)
+  )
+
+GEXTEND Gram
+  GLOBAL: gallina_ext;
+
+  ssr_export_token:
+    [ [ IDENT "Import" -> Some false
+      | IDENT "Export" -> Some true
+      |  -> None ] ]
+  ;
+
+  gallina_ext:
+    [[ IDENT "From"; ns = Constr.global;
+       IDENT "Require"; export = ssr_export_token;
+       qidl = LIST1 Constr.global ->
+       let qidl = List.map (join_reference ns) qidl in
+       Vernacexpr.VernacRequire (export, None, qidl)
+  ]];
+END
+
+
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)