diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 8963ea5e..9ed28f8b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -77,8 +77,9 @@ let rec list_try_compile f = function | [] -> anomaly "try_find_f" | h::t -> try f h - with UserError _ | TypeError _ | PretypeError _ - | Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> + with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ + | Loc.Exc_located + (_, (UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _)) -> list_try_compile f t let force_name = |