From 36fa70885150234159b0a6d8a1deb2d9fb3d2b8a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 3 Feb 2008 00:42:23 +0000
Subject: Add new files theories/Program/Basics.v and
 theories/Classes/Relations.v for basic functional programming and relation
 definitions respectively. Classes.Relations also includes the definition of
 Morphism and instances for the standard morphisms and relations (eq, iff,
 impl, inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
 has been reimplemented on top of these definitions, hence it doesn't require
 a setoid implementation anymore. It also generates obligations for missing
 reflexivity proofs, like the current setoid_rewrite. It has not been tested
 on large examples but it should handle directions and occurences. Works with
 in if no obligations are generated at this time. What's missing is being able
 to rewrite by a lemma instead of a simple hypothesis with no premises.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4a2dad8cab..a58125dc09 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1608,7 +1608,7 @@ defined in the same file:
 
 \begin{Variants}
 \item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots
-    {\ident$_n$}}\tacindex{dependent induction ... generalizing}
+    {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing}
   
   Does dependent induction on the hypothesis {\ident} but first
   generalizes the goal by the given variables so that they are
@@ -1616,9 +1616,9 @@ defined in the same file:
   to do with the variables that are inside some constructors in the
   induction hypothesis. The other ones need not be further generalized.
 
-\item {\tt dependent destruction}\tacindex{dependent destruction}
+\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction}
   
-  Does the generalization of the instance but uses {\tt destruct}
+  Does the generalization of the instance {\ident} but uses {\tt destruct}
   instead of {\tt induction} on the generalized hypothesis. This gives
   results equivalent to {\tt inversion} or {\tt dependent inversion} if
   the hypothesis is dependent.
-- 
cgit v1.2.3