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 | |
| 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')
| -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. |