+ let rec alpha_norm k = function
+ | NCic.Lambda (_,ty,t) ->
+ NCic.Lambda("_",alpha_norm k ty,alpha_norm k t)
+ | NCic.Prod (_,ty,t) ->
+ NCic.Prod("_",alpha_norm k ty,alpha_norm k t)
+ | NCic.LetIn (_,ty,t,b) ->
+ NCic.LetIn("_",alpha_norm k ty,alpha_norm k t,alpha_norm k b)
+ | NCic.Meta (_,(_,NCic.Irl _)) as t -> t
+ | NCic.Meta (n,(s,NCic.Ctx tl)) as t ->
+ let tl' = HExtlib.sharing_map (alpha_norm k) tl in
+ if tl == tl' then t else NCic.Meta (n,(s,NCic.Ctx tl'))
+ | t -> NCicUtils.map ~hbr:false (new NCicPp.status None)
+ (fun _ _ -> ()) () alpha_norm t
+