diff options
| author | Emilio Jesus Gallego Arias | 2019-07-31 21:07:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 21:11:20 +0200 |
| commit | 9b7816a80c77d7f9b4cea35f8ed983763bd8a5c7 (patch) | |
| tree | 40cf3f202cebd32a7a4ef200487425a60ad7cc42 /toplevel/ccompile.ml | |
| parent | 4e679df3c15e5e554ff9ef85138f9c55396e9f0b (diff) | |
[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`.
Diffstat (limited to 'toplevel/ccompile.ml')
| -rw-r--r-- | toplevel/ccompile.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 *) |