+
+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
+
+type pattern =
+ CicNotationPt.term Disambiguate.disambiguator_input option *
+ (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+ GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+
+