X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=4b85d61bc7960aac8f20e10953f9e3cef67a1815;hb=79fdc0d44a2c8a3b1d2649b25fd7181c2ef49209;hp=d70bd15453cea4b9562d7abf94db97d21eaf94ef;hpb=d34d7101ba59a19fa030fe9a5c6b3d563efc8f3d;p=helm.git

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 =