diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
| commit | 860dc1cb91549068cf65f963bf819f47eb13ebe4 (patch) | |
| tree | 419adf42d07f3bcc2f979eb1f42fa3cd1fd7c585 /pretyping/cases.ml | |
| parent | 12c78d4e45ccc9b923cd300f981ef205fee1c650 (diff) | |
| parent | 8232f27773f3463600fbaac0f70966bd4893ea20 (diff) | |
Merge branch 'v8.6'
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 |