;;
(* cook var term *)
-let cook curi cookingsno var =
+let cook curi cookingsno var is_letin =
let rec aux k =
let module C = Cic in
function
)
| C.Appl [] -> raise Impossible
| C.Const (uri,_) ->
- if match CicEnvironment.get_obj uri with
+ if not is_letin && match CicEnvironment.get_obj uri with
C.Definition (_,_,_,params) when mem var params -> true
| C.Definition _ -> false
| C.Axiom (_,_,params) when mem var params -> true
C.Const (uri,UriManager.relative_depth curi uri cookingsno)
| C.Abst _ as t -> t
| C.MutInd (uri,_,i) ->
- if match CicEnvironment.get_obj uri with
+ if not is_letin && match CicEnvironment.get_obj uri with
C.InductiveDefinition (_,params,_) when mem var params -> true
| C.InductiveDefinition _ -> false
| _ -> raise WrongUriToInductiveDefinition
else
C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i)
| C.MutConstruct (uri,_,i,j) ->
- if match CicEnvironment.get_obj uri with
+ if not is_letin && match CicEnvironment.get_obj uri with
C.InductiveDefinition (_,params,_) when mem var params -> true
| C.InductiveDefinition _ -> false
| _ -> raise WrongUriToInductiveDefinition
let cooked_once =
add_binder (C.Name varname) varbody vartype
(match varbody with
- Some _ -> ty
- | None -> cook curi cookingsno var ty
+ Some _ -> cook curi cookingsno var true ty
+ | None -> cook curi cookingsno var false ty
)
in
cookrec cooked_once tl
(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 =