diff options
| author | Matthieu Sozeau | 2016-08-17 16:31:32 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-08-17 18:12:21 +0200 |
| commit | 745df84bc3f32a646f6010a0b40a42023aae9cf9 (patch) | |
| tree | 7ee398b686fc1fd488360392100d0301c186024f | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Fix setoid_rewrite to raise proper errors
when the rewrite lemma doesn't typecheck or does not
correspond to a relation.
| -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 47c78ae5c2..7acad20d20 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 = |