+ let number_of_variables_without_a_body =
+ let is_not_letin uri =
+ match CicEnvironment.get_obj uri with
+ C.Variable (_,None,_) -> true
+ | C.Variable (_,Some _,_) -> false
+ | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ in
+ List.fold_left
+ (fun i uri -> if is_not_letin uri then i + 1 else i) 0 vars
+ in
+ C.InductiveDefinition
+ (dl', params, n_ind_params + number_of_variables_without_a_body)