NCic.Meta (index, (0, NCic.Ctx cic_subst))
| CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
NCic.Meta (index, (0, NCic.Ctx cic_subst))
| CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in