From f25076a11d7ede2ded6f6f57ce9a906bfa3cee27 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 17 Dec 2001 15:43:10 +0000
Subject: new command Back

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-oth.tex | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 1ad2f7efd7..c5bd636615 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -544,6 +544,26 @@ over the name of a module or of an object inside a module.
 \item \ident: \errindex{no such entry}
 \end{ErrMsgs}
 
+\subsection{\tt Back.}
+\comindex{Back}
+
+This commands undoes all the effects of the last vernacular
+command. This does not include commands that only access to the
+environment like those described in the previous sections of this
+chapter (for instance {\tt Require} and {\tt Load} can be undone, but
+not {\tt Check} and {\tt Locate}). Commands read from a vernacular
+file are considered as a single command.
+
+\begin{Variants}
+\item {\tt Back $n$} \\
+  Undoes $n$ vernacular commands.
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{Reached begin of command history} \\
+  Happens when there is vernacular command to undo.
+\end{ErrMsgs}
+
 \subsection{\tt Restore State \ident.}
 \comindex{Restore State}
   Restores the state contained in the file \str.
-- 
cgit v1.2.3