3 files changed, 33 insertions, 6 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c2f52e23bc..0346c4a555 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1242,7 +1242,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c
 
 The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command.
 
-\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}}
+\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}\optindex{Ltac Batch Debug}}
 
 The {\ltac} interpreter comes with a step-by-step debugger. The
 debugger can be activated using the command
@@ -1273,6 +1273,17 @@ r $n$: & advance $n$ steps further\\
 r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
 
+A non-interactive mode for the debugger is available via the command
+
+\begin{quote}
+{\tt Set Ltac Batch Debug.}
+\end{quote}
+
+This option has the effect of presenting a newline at every prompt,
+when the debugger is on.  The debug log thus created, which does not
+require user input to generate when this option is set, can then be
+run through external tools such as \texttt{diff}.
+
 \subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
 
 It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 56ce753cd6..3daaac88b1 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -697,8 +697,8 @@ which can be any valid path.
 
 \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
 
-This command is equivalent to the command line option {\tt -Q {\dirpath}
-  {\str}}. It adds the physical directory {\str} to the current {\Coq}
+This command is equivalent to the command line option {\tt -Q {\str}
+  {\dirpath}}. It adds the physical directory {\str} to the current {\Coq}
 loadpath and maps it to the logical directory {\dirpath}.
 
 \begin{Variants}
@@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory
 \end{Variants}
 
 \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}}
-This command is equivalent to the command line option {\tt -R {\dirpath}
-  {\str}}. It adds the physical directory {\str} and all its
+This command is equivalent to the command line option {\tt -R {\str}
+  {\dirpath}}. It adds the physical directory {\str} and all its
 subdirectories to the current {\Coq} loadpath.
 
 \begin{Variants}
@@ -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.
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 6d54b4de15..8ba28b32f1 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom.
 \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
 \label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
-  exact {\term}; Save.} That is, you have to give the full proof in
+  exact {\term}. Qed.} That is, you have to give the full proof in
 one gulp, as a proof term (see Section~\ref{exact}).
 
 \variant {\tt Proof.}