diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7516951e8..e16e8e1cc 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2257,7 +2257,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* The tycon may be ill-typed after abstraction. *) let env' = push_rel_context (context_of_arsign sign) env in ignore(Typing.sort_of env' !evdref pred); pred - with _ -> + with e when Errors.noncritical e -> let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t in Option.get tycon, pred |