| Some _, None -> assert false (* due to typing rules *))
canonical_context l))
| C.Sort s -> C.ASort (fresh_id'', s)
- | C.Implicit -> C.AImplicit (fresh_id'')
+ | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
| C.Cast (v,t) ->
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then