diff options
| author | Emilio Jesus Gallego Arias | 2019-06-10 23:06:45 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-30 17:30:04 +0200 |
| commit | bfe93b7c7b737ae2b1ccb52ffc05a5b241cc9c20 (patch) | |
| tree | 642a84e0e7860f70756ac012e73a0c2900a0e816 /toplevel | |
| parent | 38aa59e1aa2edeca7dabe4275790295559751e72 (diff) | |
[library] Move library to vernac
This is step 1 on removing library state from the lower layers.
Here we move library loading to the vernacular layer; few things
depend on it:
- printers: we add a parameter for those needing to access on-disk data,
- coqlib: indeed a few tactics do try to check that a particular
library is loaded; this is a tricky part. I've replaced that for a
module name check, but indeed this is fully equivalent due to
side-effects of `Require`. We may want to think what to do here.
A few other minor code movements were needed, but there are
self-explanatory.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqc.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 019577ac85..7658ad68a5 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -11,7 +11,7 @@ let outputstate opts = Option.iter (fun ostate_file -> let fname = CUnix.make_suffix ostate_file ".coq" in - States.extern_state fname) opts.Coqcargs.outputstate + Library.extern_state fname) opts.Coqcargs.outputstate let coqc_init _copts ~opts = Flags.quiet := true; @@ -53,7 +53,8 @@ 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 - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + 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 ()) end; CProfile.print_profile () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f09d202edf..33a95e7b30 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -87,7 +87,7 @@ let set_options = List.iter set_option let inputstate opts = Option.iter (fun istate_file -> let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in - States.intern_state fname) opts.inputstate + Library.intern_state fname) opts.inputstate (******************************************************************************) (* Fatal Errors *) |