diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3f01adf7e..934cefbfe 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -65,13 +65,14 @@ let error_wrong_numarg_constructor ?loc env c n = let error_wrong_numarg_inductive ?loc env c n = raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n)) -let rec list_try_compile f = function - | [a] -> f a - | [] -> anomaly (str "try_find_f") +let list_try_compile f l = + let rec aux errors = function + | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors) | h::t -> try f h - with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ -> - list_try_compile f t + with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + aux (e::errors) t in + aux [] l let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na |