From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 Jan 2009 17:10:50 +0000 (+0000)
Subject: we were generating a name for the main fix twice
X-Git-Tag: make_still_working~4233
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=164332b640d2c2e601350065b0074ba80426ea5c;p=helm.git

we were generating a name for the main fix twice
---

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)
   | _ -> []
 ;;