Ajout coercions dans les constructeurs et les declarations

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

2 files changed, 46 insertions, 1 deletions

diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index 186a9be732..5445224b02 100644
--- a/doc/Coercion.tex
+++ b/doc/Coercion.tex
@@ -200,6 +200,51 @@ valid coercion paths are ignored; they are signaled by a warning.
   This defines {\ident} just like \texttt{Local {\ident} :=
     {\term}}, and then declares {\ident} as a coercion between it
   source and its target.
+
+\item Assumptions can be declared as coercions at declaration
+time. This extends the grammar of declarations from Figure
+\ref{sentences-syntax} as follows:
+\comindex{Variable \mbox{\rm (and coercions)}}
+\comindex{Axiom \mbox{\rm (and coercions)}}
+\comindex{Parameter \mbox{\rm (and coercions)}}
+\comindex{Hypothesis \mbox{\rm (and coercions)}}
+
+\begin{tabular}{lcl}
+%% Declarations
+{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\
+&&\\
+{\assums} & ::= & {\simpleassums} \\
+          & $|$ & \nelist{{\tt (} \simpleassums {\tt )}}{} \\
+&&\\
+{\simpleassums} & ::= &  \nelist{\ident}{} {\tt :}\zeroone{{\tt >}} {\term}\\  
+\end{tabular}
+
+If the extra {\tt >} is present before the type of some assumptions, these
+assumptions are declared as coercions.
+
+\item Constructors of inductive types can be declared as coercions at
+definition time of the inductive type. This extends and modifies the
+grammar of inductive types from Figure \ref{sentences-syntax} as follows: 
+\comindex{Inductive \mbox{\rm (and coercions)}}
+\comindex{CoInductive \mbox{\rm (and coercions)}}
+
+\begin{center}
+\begin{tabular}{lcl}
+%% Inductives
+{\inductive} & ::= & 
+           {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
+ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
+           & & \\
+{\inductivebody} & ::= & 
+  {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\
+   && ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\
+           & & \\
+{\constructor} & ::= &  {\ident} \sequence{\binderlet}{} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\
+\end{tabular}
+\end{center}
+
+Especially, if the extra {\tt >} is present in a constructor
+declaration, this constructor is declared as a coercion.
 \end{Variants}
 
 \asubsection{\tt Identity Coercion {\ident}:{\class$_1$} >-> {\class$_2$}.} 
@@ -311,7 +356,6 @@ uniform inheritance condition is not satisfied).
 \Rem The keyword {\tt Structure}\comindex{Structure} is a synonym of {\tt
 Record}.
 
-
 \asection{Coercions and Sections}
 \index{Coercions!and sections}
   The inheritance mechanism is compatible with the section
diff --git a/doc/macros.tex b/doc/macros.tex
index 819a64d9b9..7417145ebb 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -117,6 +117,7 @@
 %% New syntax specific entries
 \newcommand{\annotation}{\nterm{annotation}}
 \newcommand{\assums}{\nterm{assums}} % vernac
+\newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions
 \newcommand{\binder}{\nterm{binder}}
 \newcommand{\binderlet}{\nterm{binderlet}}
 \newcommand{\binderlist}{\nterm{binderlist}}