From 56cf321a6a275bca6fde0cafb36b6cc9bfba0f93 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 8 Dec 2006 10:26:54 +0000
Subject: Correction typo règle réduction du fix chapitre CCI Maj mode emacs
 coqide dans faq

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

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 34b5a3fbf9..7183e040e1 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1572,7 +1572,8 @@ Let $F$ be the set of declarations: $f_1/k_1:A_1:=t_1 \ldots
 f_n/k_n:A_n:=t_n$.
 The reduction for fixpoints is:
 \[ (\Fix{f_i}{F}~a_1\ldots
-a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n}\]
+a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n}
+~a_1\ldots a_{k_i}\]
 when $a_{k_i}$ starts with a constructor.
 This last restriction is needed in order to keep strong normalization
 and corresponds to the reduction for primitive recursive operators.
-- 
cgit v1.2.3