From e1c92aa2c7870fa8fb76ea3db7e6d32215dfb846 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 18 Nov 2017 15:21:21 +0100
Subject: [PATCH] remove a useless try

---
 theories/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index fc019e62..93c64f58 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -345,7 +345,7 @@ Ltac solve_proper_prepare :=
   | |- Proper _ _ => intros ???
   | |- (_ ==> _)%signature _ _ => intros ???
   | |- pointwise_relation _ _ _ _ => intros ?
-  | |- ?R ?f _ => try let f' := constr:(λ x, f x) in intros ?
+  | |- ?R ?f _ => let f' := constr:(λ x, f x) in intros ?
   end; simplify_eq;
   (* We try with and without unfolding. We have to backtrack on
      that because unfolding may succeed, but then the proof may fail. *)
-- 
GitLab