From bb6e15cb3d64f2902f98d01b8fe12948a7191095 Mon Sep 17 00:00:00 2001 From: coq Date: Tue, 30 Dec 2003 09:53:31 +0000 Subject: modif generales claude git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/Cases.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'doc/Cases.tex') 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) -- cgit v1.2.3