diff options
author | 2015-06-28 15:02:22 +0200 | |
---|---|---|
committer | 2015-06-28 15:02:22 +0200 | |
commit | 902ce91fd6006e6df57a8d5133676981967d49b4 (patch) | |
tree | ca0a2e19e33111855c12c12b99df63a047275cec /toplevel/vernacentries.ml | |
parent | a0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d (diff) |
Reinstall Set Printing Universes option overwritten by Maxime!
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 04d572cd3..2af28de98 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1437,6 +1437,15 @@ let _ = declare_bool_option { optsync = true; optdepr = false; + optname = "printing of universes"; + optkey = ["Printing";"Universes"]; + optread = (fun () -> !Constrextern.print_universes); + optwrite = (fun b -> Constrextern.print_universes:=b) } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = Flags.get_dump_bytecode; |