if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let tys =
- List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' () =
let fl' =
| None -> if l = [] then t' () else C.Appl ((t' ())::l)
)
| C.CoFix (i,fl) ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' =
let fl' =
if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let tys =
- List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' () =
let fl' =
| None -> if l = [] then t' () else C.Appl ((t' ())::l)
)
| C.CoFix (i,fl) ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' =
let fl' =