From 1ea5bb84b302b8518ad37cef2cb05a52e73ade56 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Jul 2011 20:35:23 +0000
Subject: 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
---
 lib/flags.ml  | 2 ++
 lib/flags.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'lib')

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
-- 
cgit v1.2.3