open MatitaTypes
exception Ambiguous_input
+exception DisambiguationError of string Lazy.t list list
type choose_uris_callback =
id:string -> UriManager.uri list -> UriManager.uri list
else
drop_aliases_and_clear_diff res
in
- let rec aux =
+ let rec aux errors =
function
- | [ pass ] -> set_aliases pass (try_pass pass)
+ | [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation newerrors ->
+ raise (DisambiguationError (errors @ [newerrors])))
| hd :: tl ->
(try
set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation -> aux tl)
+ with Disambiguate.NoWellTypedInterpretation newerrors ->
+ aux (errors @ [newerrors]) tl)
| [] -> assert false
in
let saved_use_coercions = !CoercDb.use_coercions in
try
- let res = aux passes in
+ let res = aux [] passes in
CoercDb.use_coercions := saved_use_coercions;
res
with exn ->