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 ->
}
let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
{ do_it =
fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.CicUtil.profile
+ -> profiler.HExtlib.profile
(disambiguate_thing ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff) thing
}