diff options
| author | Emilio Jesus Gallego Arias | 2019-06-10 23:11:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-18 16:16:00 +0200 |
| commit | 42ff3109217452853c3b853d21f09a317dd6e37d (patch) | |
| tree | d95cc4e262956c48fe15b02ce59c6507420b305b /toplevel | |
| parent | c5ecc185ccb804e02ef78012fc6ae38c092cc80a (diff) | |
[library] Move `Declaremods` to `vernac/`
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqc.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 () |