From fb7851ec9be42e9d3b77c9f7034c3995f68b2ced Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Apr 2007 09:44:58 +0000
Subject: Ajout possibilité d'options à trois mots.

Suppression au passage syntaxe "Set table field ref", synonyme de "Add
table field ref" et de "Unset table field ref", synonyme de "Remove
table field ref".  Changement de la syntaxe "Test tabel field val" en
""Test tabel field for val".


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Natural.tex    |  6 +++---
 doc/refman/RefMan-ext.tex | 10 +++++-----
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex
index 69dfab87c6..9a9abe5dff 100644
--- a/doc/refman/Natural.tex
+++ b/doc/refman/Natural.tex
@@ -121,7 +121,7 @@ declared as implicit, type
 
 \comindex{Test Natural}
 \begin{coq_example*}
-Test Natural Implicit lem1.
+Test Natural Implicit for lem1.
 \end{coq_example*}
 
 \subsubsection*{Implicit proof constructors}
@@ -211,7 +211,7 @@ By default, the data type \verb=nat= and the inductive connectives
 
 As above, you can remove or test a constant declared implicit.  Use
 {\tt Remove Natural Contractible $id$} or {\tt Test Natural
-Contractible $id$}.
+Contractible for $id$}.
 
 \asubsection{Contractible proof steps}
 
@@ -328,7 +328,7 @@ a non inductive transparent definition.
 As for implicit and contractible definitions, you can remove or test a
 non inductive definition declared transparent.
 Use \texttt{Remove Natural Transparent} \ident or 
-\texttt{Test Natural Transparent} \ident.
+\texttt{Test Natural Transparent for} \ident.
 
 \subsubsection*{Transparent inductive definitions}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 769927cafa..f6e44f91ab 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -424,7 +424,7 @@ The default is to not print synthesisable types.
 \subsubsection{Printing matching on irrefutable pattern
 \comindex{Add Printing Let {\ident}}
 \comindex{Remove Printing Let {\ident}}
-\comindex{Test Printing Let {\ident}}
+\comindex{Test Printing Let for {\ident}}
 \comindex{Print Table Printing Let}}
 
 If an inductive type has just one constructor,
@@ -443,7 +443,7 @@ pattern-matching is written using a {\tt let} expression.
 This removes {\ident} from this list.
 
 \begin{quote}
-{\tt Test Printing Let {\ident}.}
+{\tt Test Printing Let for {\ident}.}
 \end{quote}
 This tells if {\ident} belongs to the list.
 
@@ -460,7 +460,7 @@ it is sensible to the command {\tt Reset}.
 \subsubsection{Printing matching on booleans
 \comindex{Add Printing If {\ident}}
 \comindex{Remove Printing If {\ident}}
-\comindex{Test Printing If {\ident}}
+\comindex{Test Printing If for {\ident}}
 \comindex{Print Table Printing If}}
 
 If an inductive type is isomorphic to the boolean type,
@@ -479,7 +479,7 @@ pattern-matching is written using an {\tt if} expression.
 This removes {\ident} from this list.
 
 \begin{quote}
-{\tt Test Printing If {\ident}.}
+{\tt Test Printing If for {\ident}.}
 \end{quote}
 This tells if {\ident} belongs to the list.
 
@@ -498,7 +498,7 @@ it is sensible to the command {\tt Reset}.
 This example emphasizes what the printing options offer.
 
 \begin{coq_example}
-Test Printing Let prod.
+Test Printing Let for prod.
 Print fst.
 Remove Printing Let prod.
 Unset Printing Synth.
-- 
cgit v1.2.3