diff options
Diffstat (limited to 'ltac/rewrite.ml')
| -rw-r--r-- | ltac/rewrite.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 47c78ae5c..7acad20d2 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1440,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy = fun ({ state = () } as input) -> let unify env evars t = let (sigma, cstrs) = evars in - let ans = - try Some (refresh_hypinfo env sigma c) - with e when Class_tactics.catchable e -> None - in - match ans with - | None -> None - | Some (sigma, rew) -> - let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in - match rew with - | None -> None - | Some rew -> Some rew + let (sigma, rew) = refresh_hypinfo env sigma c in + unify_eqn rew l2r flags env (sigma, cstrs) None t in let app = apply_rule unify occs in let strat = |