From 9d4f34feb780527c2adc7575f785391b35413fcc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 4 Aug 2003 14:58:32 +0000
Subject: Bug 'Set Hyps Limit'

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

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 03f01d8d7d..a65cd816e4 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -302,14 +302,14 @@ process of an {\tt Intros}.
 
 \end{Variants}
 
-\subsection{\tt Set Hyps\_limit {\num}.}
-\comindex{Set Hyps\_limit}
+\subsection{\tt Set Hyps Limit {\num}.}
+\comindex{Set Hyps Limit}
 This command sets the maximum number of hypotheses displayed in
 goals after the application of a tactic. 
 All the hypotheses remains usable in the proof development.
 
-\subsection{\tt Unset Hyps\_limit.}
-\comindex{Unset Hyps\_limit}
+\subsection{\tt Unset Hyps Limit.}
+\comindex{Unset Hyps Limit}
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-- 
cgit v1.2.3