*** empty log message ***

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

1 files changed, 12 insertions, 4 deletions

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index bf8414ca1e..5b80e4e194 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -921,8 +921,13 @@ following rules:
 \begin{description}
 \item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}}
                       {\compat{I:(x:A)A'}{(x:A)B'}}}
-\item[\Prop] \inference{\compat{I:\Prop}{I\ra\Prop}~~~~~
-   \frac{I \mbox{~is a singleton definition}}{\compat{I:\Prop}{I\ra \Set}}}
+\item[\Prop] \inference{\compat{I:\Prop}{I\ra\Prop}}
+\inference{
+   \frac{I \mbox{~is an empty or singleton
+       definition}}{\compat{I:\Prop}{I\ra \Set}}~~~~~
+   \frac{I \mbox{~is an empty or small singleton
+       definition}}{\compat{I:\Prop}{I\ra \Type(i)}}
+}
 
 \item[\Set] \inference{\frac{s \in
       \{\Prop, \Set\}}{\compat{I:\Set}{I\ra s}}
@@ -947,8 +952,9 @@ $I$.
 %problems if extracted terms are explicitly used such as in the 
 %{\tt Program} tactic or when extracting ML programs.
 
-\paragraph{Singleton elimination}
+\paragraph{Empty and singleton elimination}
 \index{Elimination!Singleton elimination}
+\index{Elimination!Empty elimination}
 
 A {\em singleton definition} has always an informative content,
 even if it is a proposition.
@@ -957,7 +963,7 @@ A {\em singleton
 definition} has only one constructor and all the argument of this
 constructor are non informative. In that case, there is a canonical
 way to interpret the informative extraction on an object in that type,
-such that the elimination on sort $s$ is legal.  Typical examples are
+such that the elimination on any sort $s$ is legal.  Typical examples are
 the conjunction of non-informative propositions and the equality. In
 that case, the term \verb!eq_rec! which was defined as an axiom, is
 now a term of the calculus.
@@ -965,6 +971,8 @@ now a term of the calculus.
 Print eq_rec.
 Extraction eq_rec.
 \end{coq_example}
+An empty definition has no constructors, in that case also,
+elimination on any sort is allowed.
 
 \paragraph{Type of branches.}
 Let $c$ be a term of type $C$, we assume $C$ is a type of constructor