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 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/flags.ml')

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