let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
Cic.MutCase (sp, i, outty', t', pl')
| Cic.Fix (i, fl) ->
- let tys = List.map
- (fun (n,_,ty,_) ->
- Some (Cic.Name n,(Cic.Decl ty))) fl in
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
let fl' = List.map
(fun (n,i,ty,bo) ->
let ty' = mk_fresh_names ~subst metasenv context ty in
(n,i,ty',bo')) fl in
Cic.Fix (i, fl')
| Cic.CoFix (i, fl) ->
- let tys = List.map
- (fun (n,_,ty) ->
- Some (Cic.Name n,(Cic.Decl ty))) fl in
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
let fl' = List.map
(fun (n,ty,bo) ->
let ty' = mk_fresh_names ~subst metasenv context ty in