From 5923919582bbfa207d5141d5059bd3916e501843 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Nov 2008 13:09:40 +0000
Subject: - Fixed minor bug #1994 in the tactic chapter of the manual [doc] -
 Improved warning when found several path to the same file in path  
 [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to
 true (i.e. eq_true)   [Datatypes.v, tactics]

PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-gal.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 28cb402f35..3e3d422638 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1427,7 +1427,7 @@ generally any mutually recursive definitions.
 \begin{Variants}
 \item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
         with {\ldots} \\
-        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\type$_m$}}\\
+        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\term$_m$}}\\
         Allows to define simultaneously {\ident$_1$}, {\ldots},
         {\ident$_m$}.
 \end{Variants}
-- 
cgit v1.2.3