in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
| C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
| C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)