Merge PR #10605: [toplevel] Make all argument lists to be in user-declared order.

Reviewed-by: herbelin

4 files changed, 30 insertions, 5 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index fe5361c156..3600658e23 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
@@ -193,7 +193,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
 
 (******************************************************************************)
@@ -205,7 +205,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 0490c35970..113b1fb5d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -547,6 +547,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                                               *)
 (******************************************************************************)
@@ -557,7 +574,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 0b5481fe72..c4e3571281 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -210,3 +210,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 e9d8263b85..bca6b48499 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -169,6 +169,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