diff options
| -rw-r--r-- | pretyping/pretyping.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 94749648e..d9f490ba5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -73,9 +73,14 @@ let search_guard loc env possible_indexes fixdefs = (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then - (* in this case, errors are delegated to the kernel, which will - check well-guardedness if required. *) - Array.of_list (List.map List.hd possible_indexes) + let indexes = Array.of_list (List.map List.hd possible_indexes) in + let fix = ((indexes, 0),fixdefs) in + (try check_fix env ~chk:true fix + with reraise -> + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); + indexes else (* we now search recursively among all combinations *) (try |