diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 |
2 files changed, 4 insertions, 6 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fbc64d95d0..28dcb00384 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -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 } diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 4dc2ade7a1..2fca83f7c6 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -363,7 +363,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p = let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = try Inl (intern_evaluable ist r) - with e when Logic.catchable_exception e -> + with e when CErrors.noncritical e -> (* Compatibility. In practice, this means that the code above is useless. Still the idea of having either an evaluable ref or a pattern seems interesting, with "head" reduction |