| 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
| _ -> assert false)
| k -> k
in
- let localization_tbl = Cic.CicHash.create 503 in
+ let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
~initial_ugraph ~aliases ~string_context_of_context
~universe ~lookup_in_library ~mk_implicit ~description_of_alias
~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~refine_thing:refine_term (text,prefix_len,term)
- ~localization_tbl
+ ~mk_localization_tbl
~hint
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let hint = (fun _ x -> x), fun k -> k in
- let localization_tbl = Cic.CicHash.create 503 in
+ let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
~aliases ~universe ~uri ~string_context_of_context
~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
~initial_ugraph:CicUniv.empty_ugraph
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj
- ~localization_tbl
+ ~mk_localization_tbl
~hint
~passes:(MultiPassDisambiguator.passes ())
~freshen_thing:CicNotationUtil.freshen_obj