From fb73dae49f461f5ec81af870ce8279d619ebef9a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 13:56:19 +0000
Subject: Added documentation: "Theorem id x1..xn : T" and "Set Automatic
 Introduction". Updated documentation in many ways: - merged binder and
 binderlet as done for a while in implementation - fixed a few technical
 problems (bad indexation of {x:A|P x}, missing   spaces in html code in many
 situations due to missing curly brackets   around TeX macros - e.g. around
 \ldots -, missing dots at end of   sentences, ...) - renamed "statement"
 commands into "assertion" commands and   "declaration" commands into
 "assumption" commands - moved Goal and Save out of the Gallina chapter -
 avoid some recovering in the Gallina and proof mode chapters - slight
 smoothing of some hard-to-read paragraphs of the manual

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

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index f7f4d95d97..b41014ab70 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -94,7 +94,7 @@ does not produce an equality, contrary to the let pattern construct
 {\tt let '(x1, ..., xn) := t in b}.
 
 The next two commands are similar to their standard counterparts
-Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
+Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
 they define constants. However, they may require the user to prove some
 goals to construct the final definitions.
 
-- 
cgit v1.2.3