Apply 2 suggestion(s) to 2 file(s)

CHANGELOG.md

@@ -8,8 +8,9 @@ API-breaking change is listed.
   `difference_difference_r` and `difference_difference_r_L`.
 - Let `set_solver` use `eauto` (instead of `idtac`) as its default solver.
 - Add tactic `tc_solve` (this was `iSolveTC` in Iris).
-- Let `f_equiv` to use `reflexivity` in a way similar to `f_equal`. That is,
-  let `f_equiv` solve goals and subgoals of the form `R x x`.
+- Change `f_equiv` to use `reflexivity` in a way similar to `f_equal`. That is,
+  let `f_equiv` solve goals and subgoals of the form `R x x`. However, we use
+  a restricted `fast_reflexivity` as full `reflexivity` can be quite expensive.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/tactics.v

@@ -438,7 +438,7 @@ Ltac f_equiv :=
   (* Similar to [f_equal] also handle the reflexivity case. *)
   | |- _ ?x ?x => fast_reflexivity
   end;
-  (* Similar to [f_equal] immediately solve trivial solve goals *)
+  (* Similar to [f_equal] immediately solve trivial goals *)
   try fast_reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.