diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 5ce5e0436c..db4a5d3cd1 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1028,7 +1028,7 @@ You can use a what is called a hints' base. \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Lemma toto1 : 1+1 = 2. ring. Qed. @@ -1124,7 +1124,7 @@ Just use the {\ring} tactic. \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. intros. ring. @@ -1138,7 +1138,7 @@ Just use the {\field} tactic. \begin{coq_example} Require Import Reals. Require Ring. -Open Local Scope R_scope. +Local Open Scope R_scope. Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. intros. field. @@ -1157,7 +1157,7 @@ Qed. \begin{coq_example} Require Import ZArith. Require Omega. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a : Z, a>0 -> a+a > a. intros. omega. @@ -1310,7 +1310,7 @@ You need to use the {\try} and {\solve} tactics. For instance: \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a b c : Z, a+b=b+a. Proof with try solve [ring]. intros... 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. |