From 745df84bc3f32a646f6010a0b40a42023aae9cf9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Aug 2016 16:31:32 +0200
Subject: Fix setoid_rewrite to raise proper errors

when the rewrite lemma doesn't typecheck or does not
correspond to a relation.
---
 ltac/rewrite.ml | 13 ++-----------
 1 file 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 = 
-- 
cgit v1.2.3