[toplevel] Make all argument lists to be in user-declared order.

As reported by Karl Palmskog, some lists of arguments were supposed to
appear in reverse order whereas others do appear in the natural order
they are declared.

Given that in some cases, such as require, order is quite important,
we make the parsing return lists in the right order so clients don't
have to care about doing `List.rev`.

1 files changed, 5 insertions, 8 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 69dbebbc57..7f3e5ecb76 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2614,13 +2614,10 @@ let dirpath_of_file f =
 
 let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 
-  let load_objs libs =
-    let rq_file (dir, from, exp) =
-      let mp = Libnames.qualid_of_string dir in
-      let mfrom = Option.map Libnames.qualid_of_string from in
-      Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
-    List.(iter rq_file (rev libs))
-  in
+  let require_file (dir, from, exp) =
+    let mp = Libnames.qualid_of_string dir in
+    let mfrom = Option.map Libnames.qualid_of_string from in
+    Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
 
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
@@ -2659,7 +2656,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   end;
 
   (* Import initial libraries. *)
-  load_objs require_libs;
+  List.iter require_file require_libs;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;