Fixed a bug which prevented mutually recursive definitions of 3 or more

functions from being added to the library

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index d70bd15453cea4b9562d7abf94db97d21eaf94ef..4b85d61bc7960aac8f20e10953f9e3cef67a1815 100644 (file)
--- 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 =