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

when printing.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 20 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 530e25096a..909151f3c5 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 6801533efa..182a50959a 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 91ae112855..f23f9750cb 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 b9965af5dd..9b19efea78 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
+
 (* Compatibility mode *)
 
 type compat_version = V8_2 | V8_3
diff --git a/lib/flags.mli b/lib/flags.mli
index 4fd042e225..da43c86782 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
 
 type compat_version = V8_2 | V8_3
 val compat_version : compat_version option ref
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index 5b88f6a553..bc0e18e570 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 ee231b0445..41f200b4fe 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 3ce85c4656..c42d7acf64 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -908,6 +908,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 ());