diff options
| author | letouzey | 2012-07-05 16:56:28 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-05 16:56:28 +0000 |
| commit | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (patch) | |
| tree | f5934c98bd6288cc485f20dd9dfeae598170697e /doc/refman | |
| parent | 8e33b709fb2225d256dccfd4b071f85144d92d45 (diff) | |
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
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
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. |