aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-06-28 15:02:22 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-06-28 15:02:22 +0200
commit902ce91fd6006e6df57a8d5133676981967d49b4 (patch)
treeca0a2e19e33111855c12c12b99df63a047275cec /toplevel/vernacentries.ml
parenta0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d (diff)
Reinstall Set Printing Universes option overwritten by Maxime!
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml9
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;