diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 33b1952c7..307e1026b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -736,12 +736,20 @@ let _ = let _ = declare_bool_option { optsync = true; - optname = "symbols printing"; + optname = "notations printing"; optkey = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations")); optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } let _ = + declare_bool_option + { optsync = true; + optname = "raw printing"; + optkey = (SecondaryTable ("Printing","All")); + optread = (fun () -> !Options.raw_print); + optwrite = (fun b -> Options.raw_print := b) } + +let _ = declare_int_option { optsync=false; optkey=PrimaryTable("Undo"); |