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