exception PathNotWellFormed
val interpretate_path :
- context:Cic.name list -> CicNotationPt.term ->
- Cic.term
+ context:Cic.name list -> CicNotationPt.term -> Cic.term
type 'a disambiguator_input = string * int * 'a
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
- CicNotationPt.obj disambiguator_input ->
+ CicNotationPt.term CicNotationPt.obj disambiguator_input ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *