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)
List.map
(function
_,Some (n,(C.ADef at)) ->
- Some (n,(C.Def (deannotate_term at)))
+ Some (n,(C.Def ((deannotate_term at),None)))
| _,Some (n,(C.ADecl at)) ->
Some (n,(C.Decl (deannotate_term at)))
| _,None -> None