Bug 2583: Update of the syntax of terms in the reference manual

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 19 insertions, 8 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index b41014ab70..fb2eb834b1 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -92,6 +92,8 @@ Program Definition id (n : nat) : { x : nat | x = n } :=
 Finally, the let tupling construct {\tt let (x1, ..., xn) := t in b}
 does not produce an equality, contrary to the let pattern construct 
 {\tt let '(x1, ..., xn) := t in b}.
+Also, ``{\term}:>'' explicitly asks the system to see {\term} in a coerced
+way.
 
 The next two commands are similar to their standard counterparts
 Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index d14895917e..6914375ee0 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -217,12 +217,12 @@ possible one (among all tokens defined at this moment), and so on.
 
 \subsection{Syntax of terms}
 
-Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
-set of terms which form the {\em Calculus of Inductive Constructions}
-(also called \CIC). The formal presentation of {\CIC} is given in
-Chapter \ref{Cic}. Extensions of this syntax are given in chapter
-\ref{Gallina-extension}. How to customize the syntax is described in
-Chapter \ref{Addoc-syntax}.
+Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic syntax of
+the terms of the {\em Calculus of Inductive Constructions} (also
+called \CIC). The formal presentation of {\CIC} is given in Chapter
+\ref{Cic}. Extensions of this syntax are given in chapter
+\ref{Gallina-extension}. How to customize the syntax is described in Chapter
+\ref{Addoc-syntax}.
 
 \begin{figure}[htbp]
 \begin{centerframe}
@@ -240,9 +240,13 @@ Chapter \ref{Addoc-syntax}.
  & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem}
          {\tt :=} {\term}
          {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
+ & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term}
+        \zeroone{\returntype} {\tt in} {\term} & (\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term}
          {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt <:} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt :>} &(\ref{Program})\\
  & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
  & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
  & $|$ & {\tt @} {\qualid} \sequence{\term}{}
@@ -256,6 +260,7 @@ Chapter \ref{Addoc-syntax}.
  & $|$ & {\sort} &(\ref{Gallina-sorts})\\
  & $|$ & {\num} &(\ref{numerals})\\
  & $|$ & {\_} &(\ref{hole})\\
+ & $|$ & {\tt (} {\term} {\tt )} & \\
  & & &\\
 {\termarg} & ::= & {\term} &\\
  & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
@@ -496,6 +501,10 @@ arguments is used for making explicit the value of implicit arguments
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It enforces the type of {\term} to be {\type}.
 
+``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option
+{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that
+{\term} has type {\type}.
+
 \subsection{Inferable subterms
 \label{hole}
 \index{\_}}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index e2841ad649..5b1ad1981b 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -932,7 +932,7 @@ a {\tt Timeout} are unaffected.
 
 \subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
 
-This command turns off the use of a defaut timeout.
+This command turns off the use of a default timeout.
 
 \subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
 
@@ -985,7 +985,7 @@ compares applicative terms while the other is a brute-force but efficient
 algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
 similar to the bytecode representation used in the ZINC virtual
-machine~\cite{Leroy90}. It is specially useful for intensive
+machine~\cite{Leroy90}. It is especially useful for intensive
 computation of algebraic values, such as numbers, and for reflexion-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.