diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2cb6f3918f..40cd1a29c9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1413,6 +1413,24 @@ let _ = let _ = declare_int_option + { optsync = false; + optdepr = false; + optname = "the hypotheses limit"; + optkey = ["Hyps";"Limit"]; + optread = Flags.print_hyps_limit; + optwrite = Flags.set_print_hyps_limit } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "display compact goal contexts"; + optkey = ["Printing";"Compact";"Contexts"]; + optread = (fun () -> Printer.get_compact_context()); + optwrite = (fun b -> Printer.set_compact_context b) } + +let _ = + declare_int_option { optsync = true; optdepr = false; optname = "the printing depth"; |