diff options
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 e2d40f23fe..47753c1582 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 1f76e3315f..a677eb93ed 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 e721517771..37ad387da6 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 |