(** {2 Disambiguation interface} *)
(* the integer is an offset to be added to each location *)
+(* list of located error messages, each list is a tuple:
+ * - environment in string form
+ * - environment patch
+ * - location
+ * - error message
+ * - significancy of the error message, if false the error is likely to be
+ * useless for the final user ... *)
exception NoWellTypedInterpretation of
int *
((Token.flocation list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t) list
+ Token.flocation option * string Lazy.t * bool) list
exception PathNotWellFormed
val interpretate_path :
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 *