From c526b81a9a682edf2270cb544e61fe60355003dc Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 13 Mar 2013 00:00:49 +0000 Subject: Restrict (try...with...) to avoid catching critical exn (part 13) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/himsg.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/himsg.ml') 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 -- cgit v1.2.3