diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fbc64d95d0..321b05b97c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -129,7 +129,7 @@ let find_class_proof proof_type proof_method env evars carrier relation = let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in if extends_undefined (goalevars evars) evars' then raise Not_found else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] - with e when Logic.catchable_exception e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found (** Utility functions *) @@ -724,8 +724,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let rew = if l2r then rew else symmetry env sort rew in Some rew with - | e when Class_tactics.catchable e -> None - | Reduction.NotConvertible -> None + | e when noncritical e -> None let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = try @@ -741,8 +740,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = let rew = if l2r then rew else symmetry env sort rew in Some rew with - | e when Class_tactics.catchable e -> None - | Reduction.NotConvertible -> None + | e when noncritical e -> None type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } |