diff options
| author | jforest | 2006-07-13 17:14:47 +0000 |
|---|---|---|
| committer | jforest | 2006-07-13 17:14:47 +0000 |
| commit | 716148d9c71f773699146d1283791ad527b1d4fc (patch) | |
| tree | 1383f9ece90e1c9f6a7f1c594b3f445a770b0811 | |
| parent | d28d0d70a2c24bc4ecd3951ca58de84c3614e2b7 (diff) | |
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
| -rw-r--r-- | contrib/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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' |