The Coq mailing list

[tom.prince AT ualberta.net]

From: Tom Prince 
<tom.prince AT ualberta.net>

This option disables the use of the '{| field := ... |}' notation
when printing.

Signed-off-by: Tom Prince 
<tom.prince AT ualberta.net>
---

 CHANGES                      |    1 +
 doc/refman/RefMan-ext.tex    |    5 +++++
 interp/constrextern.ml       |    2 +-
 lib/flags.ml                 |    2 ++
 lib/flags.mli                |    1 +
 test-suite/output/Record.out |    8 ++++++++
 test-suite/output/Record.v   |   11 +++++++++++
 tools/coq-syntax.el          |    1 +
 toplevel/ide_slave.ml        |    1 +
 toplevel/vernacentries.ml    |    8 ++++++++
 10 files changed, 39 insertions(+), 1 deletions(-)
 create mode 100644 test-suite/output/Record.out
 create mode 100644 test-suite/output/Record.v

diff --git a/CHANGES b/CHANGES
index 54b4430..649c43f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,7 @@ Specification language and notations
   applications (use eta expanded form with explicit { } instead).
 - Added support for recursive notations with binders (allows for instance
   to write "exists x y z, P").
+- Structure/Record printing can be disable by "Unset Printing Records".
 
 Tactics
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 6801533..182a509 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -200,6 +200,11 @@ Definition b := {| x := 5; y := 3 |}.
 Definition c := {| y := 3; x := 5 |}.
 \end{coq_example}
 
+This syntax can be disabled for printing by
+\begin{quote}
+{\tt Unset Printing Records.}
+\end{quote}
+
 This syntax can also be used for pattern matching.
 
 \begin{coq_example}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 91ae112..f23f975 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -550,7 +550,7 @@ let rec extern inctx scopes vars r =
               extern_args (extern true) (snd scopes) vars args subscopes in
             begin
               try
-                if !Flags.raw_print then raise Exit;
+                if !Flags.raw_print or not !Flags.record_print then raise 
Exit;
                 let cstrsp = match ref with ConstructRef c -> c | _ -> raise 
Not_found in
                 let struc = Recordops.lookup_structure (fst cstrsp) in
                 let projs = struc.Recordops.s_PROJ in
diff --git a/lib/flags.ml b/lib/flags.ml
index 45ca062..54bfb40 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -34,6 +34,8 @@ let load_proofs = ref Lazy
 
 let raw_print = ref false
 
+let record_print = ref true
+
 let allow_inconsistent_universes = ref false
 
 (* Compatibility mode *)
diff --git a/lib/flags.mli b/lib/flags.mli
index a07612c..080ac7f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -24,6 +24,7 @@ type load_proofs = Force | Lazy | Dont
 val load_proofs : load_proofs ref
 
 val raw_print : bool ref
+val record_print : bool ref
 
 val allow_inconsistent_universes : bool ref
 
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
new file mode 100644
index 0000000..a3c63ea
--- /dev/null
+++ b/test-suite/output/Record.out
@@ -0,0 +1,8 @@
+{| field := 5 |}
+     : test
+{| field := 5 |}
+     : test
+build 5
+     : test
+build 5
+     : test
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
new file mode 100644
index 0000000..4ae4338
--- /dev/null
+++ b/test-suite/output/Record.v
@@ -0,0 +1,11 @@
+Record test := build { field : nat }.
+
+Set Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
+
+Unset Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index 5b88f6a..bc0e18e 100644
--- a/tools/coq-syntax.el
+++ b/tools/coq-syntax.el
@@ -497,6 +497,7 @@
      ("Set Printing Synth" nil "Set Printing Synth" t 
"Set\\s-+Printing\\s-+Synth")
      ("Set Printing Wildcard" nil "Set Printing Wildcard" t 
"Set\\s-+Printing\\s-+Wildcard")
      ("Set Printing All" "sprall" "Set Printing All" t 
"Set\\s-+Printing\\s-+All")
+     ("Set Printing Records" nil "Set Printing Records" t 
"Set\\s-+Printing\\s-+Records")
      ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit")
      ("Set Printing Coercions" nil "Set Printing Coercions." t 
"Set\\s-+Printing\\s-+Coercions")
      ("Set Printing Notations" "sprn" "Set Printing Notations" t 
"Set\\s-+Printing\\s-+Notations")
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 3aa2744..dfabfb1 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -32,6 +32,7 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Synth"];
   ["Printing";"Notations"];
   ["Printing";"All"];
+  ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
   ["Printing";"Universes"]]
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 769f101..2c40974 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -928,6 +928,14 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optname  = "record printing";
+      optkey   = ["Printing";"Records"];
+      optread  = (fun () -> !Flags.record_print);
+      optwrite = (fun b -> Flags.record_print := b) }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
       optname  = "use of virtual machine inside the kernel";
       optkey   = ["Virtual";"Machine"];
       optread  = (fun () -> Vconv.use_vm ());
-- 
1.7.5.2