From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 2 Jul 2008 15:12:24 +0000 (+0000)
Subject: Fixed a bug which prevented mutually recursive definitions of 3 or more
X-Git-Tag: make_still_working~4967
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79fdc0d44a2c8a3b1d2649b25fd7181c2ef49209;p=helm.git

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 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 =