diff options
| author | herbelin | 2007-04-29 09:44:58 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-29 09:44:58 +0000 |
| commit | fb7851ec9be42e9d3b77c9f7034c3995f68b2ced (patch) | |
| tree | e34c6a91a2ea9be6a1741d54688a8f38810ad3d2 /doc/refman/RefMan-ext.tex | |
| parent | 42147c4437754601b7a420facc3b0bdf1ea5ea6e (diff) | |
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
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 10 |
1 files changed, 5 insertions, 5 deletions
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. |