diff options
| -rw-r--r-- | stm/stm.ml | 13 | ||||
| -rw-r--r-- | toplevel/ccompile.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 19 | ||||
| -rw-r--r-- | toplevel/coqcargs.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
5 files changed, 35 insertions, 13 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 7f0632bd7c..1042061021 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2617,13 +2617,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; @@ -2662,7 +2659,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 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 |