From 201def788a3cac497134f460b90eb33bd5f80cce Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 16 Oct 2007 14:57:13 +0000
Subject:  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
---
 doc/refman/RefMan-tac.tex | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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}
-- 
cgit v1.2.3