- Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
+ let fix = Cic.Fix (!counter,funs) in
+ match cic with
+ Cic.Rel 1 -> fix
+ | (Cic.Appl (Cic.Rel 1::l)) ->
+ (try
+ let l' =
+ List.map
+ (function t ->
+ let t',subst,metasenv =
+ CicMetaSubst.delift_rels [] [] 1 t
+ in
+ assert (subst=[]);
+ assert (metasenv=[]);
+ t') l
+ in
+ Cic.Appl (fix::l')
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ Cic.LetIn (Cic.Name var, fix, cic))
+ | _ -> Cic.LetIn (Cic.Name var, fix, cic))