diff --git a/theories/tactics.v b/theories/tactics.v
index fc019e625bd657cf01d4932f77d0a0a51e3cfd95..93c64f589c906e9360c381c6342476507b9649dd 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. *)