Cic.context ->
((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
+
+val disambiguate_nterm :
+ NCic.term option -> LexiconEngine.status ->
+ NCic.context -> NCic.metasenv -> NCic.substitution ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+ NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term