diff --git a/theories/tactics.v b/theories/tactics.v
index 5763d58fd7ab51173f7a53d8f9390bca46c7657e..55d308f5019d8a857d1bdd03615c03a31c9548b6 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -319,6 +319,7 @@ Ltac f_equiv :=
   | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
   end;
   try simple apply reflexivity.
+Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 
 (* The tactic [solve_proper_unfold] unfolds the first head symbol, so that
 we proceed by repeatedly using [f_equiv]. *)