]> matita.cs.unibo.it Git - helm.git/commitdiff
we were generating a name for the main fix twice
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Jan 2009 17:10:50 +0000 (17:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Jan 2009 17:10:50 +0000 (17:10 +0000)
helm/software/components/library/cicFix.ml

index 21a2fdb20446594b3539d9de30f4815cb335ea96..21cb990939027695a0a8f2e21be3da66098ca65a 100644 (file)
@@ -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)
   | _ -> []
 ;;