From 164332b640d2c2e601350065b0074ba80426ea5c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 26 Jan 2009 17:10:50 +0000 Subject: [PATCH] we were generating a name for the main fix twice --- helm/software/components/library/cicFix.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) | _ -> [] ;; -- 2.39.2