From 79fdc0d44a2c8a3b1d2649b25fd7181c2ef49209 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 2 Jul 2008 15:12:24 +0000 Subject: [PATCH] Fixed a bug which prevented mutually recursive definitions of 3 or more functions from being added to the library --- .../software/components/library/librarySync.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index d70bd1545..4b85d61bc 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -480,31 +480,31 @@ let List.fold_right (fun (name,idx,ty,bo) (n,uris) -> if name = name_to_avoid then - (n+1,uris) + (n-1,uris) else let uri = UriManager.uri_of_string (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.Fix (n,funs) in + let bo = Cic.Fix (n-1,funs) in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj uri obj refinement_toolkit; - (n+1,uri::uris) - ) funs (1,[])) + (add_single_obj uri obj refinement_toolkit; + (n-1,uri::uris))) + funs (List.length funs,[])) | Cic.CoFix (_,funs) -> snd ( List.fold_right (fun (name,ty,bo) (n,uris) -> if name = name_to_avoid then - (n+1,uris) + (n-1,uris) else let uri = UriManager.uri_of_string (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.CoFix (n,funs) in + let bo = Cic.CoFix (n-1,funs) in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in add_single_obj uri obj refinement_toolkit; - (n+1,uri::uris) - ) funs (1,[])) + (n-1,uri::uris) + ) funs (List.length funs,[])) | _ -> assert false let add_obj refinement_toolkit uri obj = -- 2.39.2