open MatitaTypes
exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
exception DisambiguationError of
- (Token.flocation option * string Lazy.t) list list
+ int * (Token.flocation option * string Lazy.t) list list
type choose_uris_callback =
id:string -> UriManager.uri list -> UriManager.uri list
| [ pass ] ->
(try
set_aliases pass (try_pass pass)
- with Disambiguate.NoWellTypedInterpretation newerrors ->
- raise (DisambiguationError (errors @ [newerrors])))
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
| hd :: tl ->
(try
set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation newerrors ->
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
aux (errors @ [newerrors]) tl)
| [] -> assert false
in