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
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

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