From 8ae0762db0616e1ff177335c9fc73c816634fc89 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Feb 2021 16:20:08 +0100
Subject: [notation] option to fine tune printing of literals

---
 vernac/vernacentries.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 38ca836b32..e8d84a67a3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1565,6 +1565,13 @@ let () =
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
+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;
-- 
cgit v1.2.3