X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicFix.ml;h=21cb990939027695a0a8f2e21be3da66098ca65a;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=21a2fdb20446594b3539d9de30f4815cb335ea96;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git

diff --git a/helm/software/components/library/cicFix.ml b/helm/software/components/library/cicFix.ml
index 21a2fdb20..21cb99093 100644
--- a/helm/software/components/library/cicFix.ml
+++ b/helm/software/components/library/cicFix.ml
@@ -44,7 +44,7 @@ let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj =
             let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
             let lemmas = add_obj uri obj in
             (n-1,lemmas @ uri::uris))
-         funs (List.length funs,[]))
+         (List.tl funs) (List.length funs,[]))
     | Cic.CoFix (_,funs) ->
        snd (
         List.fold_right
@@ -59,7 +59,7 @@ let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj =
             let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
             let lemmas = add_obj uri obj in
              (n-1,lemmas @ uri::uris)) 
-          funs (List.length funs,[]))
+          (List.tl funs) (List.length funs,[]))
     | _ -> assert false)
   | _ -> []
 ;;