diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 5 |
2 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 113b1fb5d7..acbd96f699 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -178,7 +178,8 @@ let add_compat_require opts v = match v with | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false) | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} @@ -497,7 +498,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }}} - |"-test-mode" -> Vernacentries.test_mode := true; oval + |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7658ad68a5..642dc94ab2 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -54,7 +54,10 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in let library_accessor = Library.indirect_accessor in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () |