diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:17 +0000 |
| commit | 9aecb4427f0f8ca3cb4c26bc7f73bb74164a93d9 (patch) | |
| tree | 36a4ab30f4a75e73c9f4921cca1d25d1cb7cd545 /interp | |
| parent | 552df1605233769ad3cdabaadaa0011605e79797 (diff) | |
Restrict (try...with...) to avoid catching critical exn (part 8)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 9 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 6 |
3 files changed, 9 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e2d40f23f..47753c158 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -228,10 +228,10 @@ let make_notation_gen loc ntn mknot mkprim destprim l = match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) - with _ -> mknot (loc,ntn,[])) + with Failure _ -> mknot (loc,ntn,[])) | [Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.of_string x)) - with _ -> mknot (loc,ntn,[])) + with Failure _ -> mknot (loc,ntn,[])) | _ -> mknot (loc,ntn,l) @@ -810,12 +810,13 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function match f with | GRef (_,ref) -> let subscopes = - try List.skipn n (find_arguments_scope ref) with _ -> [] in + try List.skipn n (find_arguments_scope ref) + with Failure _ -> [] in let impls = let impls = select_impargs_size (List.length args) (implicits_of_global ref) in - try List.skipn n impls with _ -> [] in + try List.skipn n impls with Failure _ -> [] in subscopes,impls | _ -> [], [] in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1f76e3315..a677eb93e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -645,7 +645,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; GRef (loc, ref), impls, scopes, [] - with _ -> + with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] diff --git a/interp/notation.ml b/interp/notation.ml index e72151777..37ad387da 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -928,7 +928,7 @@ let _ = let with_notation_protection f x = let fs = freeze () in try let a = f x in unfreeze fs; a - with e -> - let e = Errors.push e in + with reraise -> + let reraise = Errors.push reraise in let () = unfreeze fs in - raise e + raise reraise |