in
C.Meta (n, l')
| C.ASort (_,s) -> C.Sort s
- | C.AImplicit _ -> C.Implicit
+ | C.AImplicit (_, annotation) -> C.Implicit annotation
| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
| C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)