diff --git a/theories/list.v b/theories/list.v
index 2de2b7b5d24007a44bf44c40f21d48b0def155aa..36f0173d7eb12abb915b8c92958f448e1889474c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3113,7 +3113,7 @@ Section mapM.
     (∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
   Proof.
     intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
-      simplify_option_eq; f_equiv; eauto.
+      simplify_option_eq; try f_equiv; eauto.
   Qed.
 End mapM.
 
diff --git a/theories/tactics.v b/theories/tactics.v
index 5c1143aa23af07a8d0fe681e39fd5e13155267f9..250f8651b6aac121974be848279543453e815b7d 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -272,7 +272,6 @@ when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
 favor the second because the relation (dist) stays the same. *)
 Ltac f_equiv :=
   match goal with
-  | _ => reflexivity
   | |- pointwise_relation _ _ _ _ => intros ?
   (* We support matches on both sides, *if* they concern the same variable, or
      variables in some relation. *)