From 716148d9c71f773699146d1283791ad527b1d4fc Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 13 Jul 2006 17:14:47 +0000
Subject: bug correction when defining graph of fixpoints/definitions not
 generated by F unction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9050 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index dffc812093..77c9de92c8 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -629,7 +629,7 @@ let make_graph (f_ref:global_reference) =
 			    let n' = 
 			      List.fold_left 
 				(fun n (nal,t'') -> 
-				   n+List.length nal) n nal_ta' 
+				   n+List.length nal) 0 nal_ta' 
 			    in
 (* 			    assert (n'<= n);  *)
 			    chop_n_arrow (n - n') t'
-- 
cgit v1.2.3