# HG changeset patch
# User paulson
# Date 846150103 -7200
# Node ID 4e8644805af22a479235136c5b1d22a8263160fe
# Parent  33f3d40145e81c1b39921a1f8ad8953faefe75a8
Documents the use of negative arguments to choplev and prlev

diff -r 33f3d40145e8 -r 4e8644805af2 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Thu Oct 24 10:43:38 1996 +0200
+++ b/doc-src/Ref/goals.tex	Thu Oct 24 11:41:43 1996 +0200
@@ -215,7 +215,9 @@
 can cancel it.
 
 \item[\ttindexbold{choplev} {\it n};] 
-truncates the state list to level~{\it n}. 
+truncates the state list to level~{\it n}, if $n\geq0$.  A negative value
+of~$n$ refers to the $n$th previous level: 
+\hbox{\verb|choplev ~1|} has the same effect as {\tt chop}.
 
 \item[\ttindexbold{back}();]
 searches the state list for a non-empty branch point, starting from the top
@@ -257,8 +259,9 @@
 prints the current proof state.
 
 \item[\ttindexbold{prlev} {\it n};] 
-prints the proof state at level {\it n}.  This allows you to review the
-previous steps of the proof.
+prints the proof state at level {\it n}, if $n\geq0$.  A negative value
+of~$n$ refers to the $n$th previous level.  This command allows
+you to review earlier stages of the proof.
 
 \item[\ttindexbold{goals_limit} := {\it k};] 
 specifies~$k$ as the maximum number of subgoals to print.