From a46ccd71539257bb55dcddd9ae8510856a5c9a16 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 Jul 2012 16:56:28 +0000
Subject: Open Local Scope ---> Local Open Scope, same with Notation and alii

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

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ff85b629b1..465ee925ee 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4091,7 +4091,7 @@ the tactic.
   No database name is given: the hint is registered in the {\tt core} 
     database. 
 
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
    \ident$_1$ \ldots\ \ident$_n$
 
   This is used to declare hints that must not be exported to the other
@@ -4099,7 +4099,7 @@ the tactic.
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
 
-\item\texttt{Hint Local} \textsl{hint\_definition} 
+\item\texttt{Local Hint} \textsl{hint\_definition}
 
   Idem for the {\tt core} database.
     
-- 
cgit v1.2.3