* added a subsection to explain the automatic declaration of schemes:

  * Set\Unset Elimination Schemes to switch on/off the declaration of standard
    elimination schemes
  * Set\Unset Equality Scheme to switch on/off the declaration of the boolean
    equality

* added a \Rem in injection to explain that if we managed to get a boolean
  equality, injection can finally work well with dependant pairs



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

1 files changed, 21 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a51e97d952..1ba08344cb 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2283,6 +2283,12 @@ Abort.
 Beware that \texttt{injection} yields always an equality in a sigma type
 whenever the injected object has a dependent type.
 
+\Rem There is a special case for dependant pairs. If we have a decidable 
+equality over the type of the first argument, then it is safe to do 
+the projection on the second one, and so {\tt injection} will work fine.
+To define such an equality, you have to use the {\tt Scheme} command 
+(see \ref{Scheme}).
+
 \Rem If {\ident} does not denote an hypothesis in the local context
 but refers to an hypothesis quantified in the goal, then the
 latter is first introduced in the local context using
@@ -3669,6 +3675,21 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
 \SeeAlso Section~\ref{Scheme-examples}
 
+\subsection{Automatic declaration of schemes}
+\comindex{Set Equality Scheme}
+\comindex{Set Elimination Schemes}
+It is possible to desactive the automatic declaration of the induction
+ principles when defining a new inductive type  with the
+ {\tt UnSet Elimination Schemes} command. It may be
+reactivated at any time with {\tt Set Elimination Schemes}. 
+\\
+
+You can also activate the automatic declaration of those boolean equalities 
+(see the second variant of {\tt Scheme})  with the {\tt Set Equality Scheme}
+ command. However you have to be carefull with this option since
+\Coq~ may now reject well-defined inductive types because it cannot compute
+a boolean equality for them.
+
 \subsection{\tt Combined Scheme\label{CombinedScheme}
 \comindex{Combined Scheme}}
 The {\tt Combined Scheme} command is a tool for combining