Added the doc for the new Scheme Equality command

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

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 90b3d1b2e5..335cc3f155 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3389,6 +3389,21 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
   Same as before but defines a non-dependent elimination principle more
   natural in case of inductively defined relations. 
+
+\item {\tt Scheme Equality for \ident$_1$}
+
+  Tries to generate an boolean equality and a proof of the
+  decidability of the usual equality.
+
+\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\\
+        with Induction for {\ident$_m$} Sort
+        {\sort$_m$}}
+
+  If you do not provide the name of the schemes, they will be automatically 
+  computed from the sorts involved (works also with Minimality).
+
 \end{Variants}
 
 \SeeAlso \ref{Scheme-examples}