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