From 8813fcac6b29aee2339fd3db3e81f0ee653b8635 Mon Sep 17 00:00:00 2001
From: mohring
Date: Sun, 21 Dec 2003 15:46:50 +0000
Subject: *** empty log message ***

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

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 006a3cd437..7cc9061877 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -1241,7 +1241,8 @@ calls are done on variables coming from patterns and representing subterms.
 
 For instance in the case of natural numbers, a proof of the induction
 principle of type 
-\[\forall P:\nat\ra\Prop, (P~\nO)\ra((n:\nat)(P~n)\ra(P~(\nS~n)))\ra(n:\nat)(P~n)\]
+\[\forall P:\nat\ra\Prop, (P~\nO)\ra((n:\nat)(P~n)\ra(P~(\nS~n)))\ra
+\forall n:\nat, (P~n)\]
 can be represented by the term:
 \[\begin{array}{l}
 \lb P:\nat\ra\Prop\mto\lb f:(P~\nO)\mto \lb g:(\forall n:\nat,
-- 
cgit v1.2.3