aboutsummaryrefslogtreecommitdiff
path: root/doc/Cases.tex
diff options
context:
space:
mode:
authorcoq2003-12-30 09:53:31 +0000
committercoq2003-12-30 09:53:31 +0000
commitbb6e15cb3d64f2902f98d01b8fe12948a7191095 (patch)
treecbc0a0f8e740505fb14d13daa47a30070ff258ea /doc/Cases.tex
parentc15a7826ecaa05bb36e934237b479c7ab2136037 (diff)
modif generales claude
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Cases.tex')
-rw-r--r--doc/Cases.tex3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/Cases.tex b/doc/Cases.tex
index aacdd0c800..a8ab494c77 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -409,7 +409,8 @@ Set Printing Depth 50.
\begin{coq_example}
Fixpoint concat
- (n: nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) :=
+ (n:nat) (l:listn n) (m:nat)
+ (l':listn m) {struct l} : listn (n + m) :=
match l, l' with
| niln, x => x
| consn n' a y, x => consn (n' + m) a (concat n' y m x)