diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 38ca836b32..e8d84a67a3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1568,6 +1568,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Raw";"Literals"]; + optread = (fun () -> !Constrextern.print_raw_literal); + optwrite = (fun b -> Constrextern.print_raw_literal := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } |