diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d9f8f52c8..2af28de982 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -424,7 +424,9 @@ let vernac_syntax_extension locality local = let local = enforce_module_locality locality local in Metasyntax.add_syntax_extension local -let vernac_delimiters = Metasyntax.add_delimiters +let vernac_delimiters sc = function + | Some lr -> Metasyntax.add_delimiters sc lr + | None -> Metasyntax.remove_delimiters sc let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) @@ -1435,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; |