| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
+ | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
| CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~mk_choice ~env
(DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
- | _ -> assert false (* god bless Bologna *)
+ | CicNotationPt.Variable _
+ | CicNotationPt.Magic _
+ | CicNotationPt.Layout _
+ | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term