Merge PR #13840: [notation] option to fine tune printing of literals

Reviewed-by: SkySkimmer
Ack-by: jfehrle

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) }