[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`.

5 files changed, 35 insertions, 13 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;
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index d8a3dbb4bb..f4a0e594fc 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -39,7 +39,7 @@ let load_vernacular opts ~state =
       if !Flags.beautify
       then Flags.with_option Flags.beautify_file load_vernac f_in
       else load_vernac s
-    ) state (List.rev opts.pre.load_vernacular_list)
+    ) state opts.pre.load_vernacular_list
 
 let load_init_vernaculars opts ~state =
   let state = load_init_file opts ~state in
@@ -198,7 +198,7 @@ let compile_file opts copts (f_in, echo) =
     compile opts copts ~echo ~f_in ~f_out
 
 let compile_files opts copts =
-  let compile_list = List.rev copts.compile_list in
+  let compile_list = copts.compile_list in
   List.iter (compile_file opts copts) compile_list
 
 (******************************************************************************)
@@ -210,7 +210,7 @@ let check_vio_tasks copts =
         let f_in = ensure ".vio" f f in
         ensure_exists f_in;
         Vio_checking.check_vio (n,f_in) && acc)
-      true (List.rev copts.vio_tasks) in
+      true copts.vio_tasks in
   if not rc then fatal_error Pp.(str "VIO Task Check failed")
 
 (* vio files *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index eb0331d95e..c99ca9f5b5 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -552,6 +552,23 @@ let parse_args ~help ~init arglist : t * string list =
     parse init
   with any -> fatal_error any
 
+(* We need to reverse a few lists *)
+let parse_args ~help ~init args =
+  let opts, extra = parse_args ~help ~init args in
+  let opts =
+    { opts with
+      pre = { opts.pre with
+              ml_includes = List.rev opts.pre.ml_includes
+            ; vo_includes = List.rev opts.pre.vo_includes
+            ; vo_requires = List.rev opts.pre.vo_requires
+            ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+            }
+    ; config = { opts.config with
+                 set_options = List.rev opts.config.set_options
+               } ;
+    } in
+  opts, extra
+
 (******************************************************************************)
 (* Startup LoadPath and Modules                                               *)
 (******************************************************************************)
@@ -562,7 +579,7 @@ let require_libs opts =
   if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
 let cmdline_load_path opts =
-  List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes)
+  opts.pre.ml_includes @ opts.pre.vo_includes
 
 let build_load_path opts =
   Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 5cced2baac..3dc11c0209 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -199,3 +199,11 @@ let parse arglist : t =
     check_compilation_output_name_consistency args;
     args
   with any -> fatal_error any
+
+let parse args =
+  let opts = parse args in
+  { opts with
+    compile_list = List.rev opts.compile_list
+  ; vio_tasks = List.rev opts.vio_tasks
+  ; vio_files = List.rev opts.vio_files
+  }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7a59a4dd12..ef8d98c219 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -174,6 +174,6 @@ let beautify_pass ~doc ~comments ~ids ~filename =
 let load_vernac ~echo ~check ~interactive ~state filename =
   let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in
   (* Pass for beautify *)
-  if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
+  if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename;
   (* End pass *)
   ostate