From 06f3ce00971283d2718e272ec9f123430d75ffa6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 11 May 2017 15:16:21 +0200
Subject: Documenting Printing Compact Contexts + CHANGES

---
 CHANGES                   |  6 ++++++
 doc/refman/RefMan-oth.tex | 16 ++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..9318a0df11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Tactics
     be fairly uncommon.
 - "auto with real" can now discharge comparisons of literals
 
+Vernacular Commands
+
+- Goals context can be printed in a more compact way when "Set
+  Printing Compact Contexts" is activated.
+
+
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 56ce753cd6..0f6978b255 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -960,6 +960,22 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command resets the displaying of goals contexts to non compact
+mode (default at the time of writing this documentation). Non compact
+means that consecutive variables of different types are printed on
+different lines.
+
+\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command sets the displaying of goals contexts to compact mode.
+The printer tries to reduce the vertical size of goals contexts by
+putting several variables (even if of different types) on the same
+line provided it does not exceed the printing width (See {\tt Set
+  Printing Width} above).
+
+\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command displays the current state of compaction of goal d'isolat.
+
 \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
 This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
 line when {\tt -emacs} is passed.
-- 
cgit v1.2.3