diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4c2e06331..87df8a055 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -350,7 +350,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." - with _ -> mt ()) + with e when Errors.noncritical e -> mt ()) let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = Evarutil.jv_nf_evar sigma vdefj in |