) l
in
C.Meta(i,l')
+ | C.Sort (C.Type u) ->
+ CicUniv.assert_univ u;
+ C.Sort (C.Type (CicUniv.recons_univ u))
| C.Sort _ as t -> t
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
in
C.CoFix (i, liftedfl)
in
- function
+ function
C.Constant (name,bo,ty,params,attrs) ->
let bo' =
match bo with