[C.Rel k])
else
C.Const (uri,UriManager.relative_depth curi uri cookingsno)
- | C.Abst _ as t -> t
| C.MutInd (uri,_,i) ->
if not is_letin && match CicEnvironment.get_obj uri with
C.InductiveDefinition (_,params,_) when mem var params -> true
(name,inductive,cook_prod curi cookingsno arity vars,constructors')
) dl
in
- C.InductiveDefinition (dl', params, n_ind_params + List.length vars)
+ 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)
;;
let cook_obj obj uri =