diff options
| author | Hugo Herbelin | 2020-03-02 21:13:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-13 07:37:25 +0100 |
| commit | cd4253ee5db24873ea131554c80650ed6d5dbd13 (patch) | |
| tree | 6702b8031bfde8b9f23f6b99853e3d95b60f5275 /plugins/ltac | |
| parent | 357f0b36bf352b26aeb5ca5c413c7bd03f615513 (diff) | |
Replacing catchable_exception by noncritical in try-with blocks.
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 |