replace by tac should not mask tac's failure message

[JasonGross]

Description of the problem

Goal True.
  assert_succeeds replace True with False.
  Fail replace True with False; [ | exact I ].
  (* The command has indeed failed with message:
Ltac call to "exact (uconstr)" failed.
The term "I" has type "True" while it is expected to have type "False = True".
*)
  replace True with False by exact I.
  (* Error:
Ltac call to "replace (uconstr) with (constr) (clause_dft_concl) (by_arg_tac)" failed.
No applicable tactic.
   *)

Coq Version

8.19+alpha (61ee398)

[SkySkimmer]

It seems to be because replace x with y by tac runs first [assumption | symmetry;assumption | tac] on the subgoal and first eats the error. (first eating the error makes sense IMO)
cf

coq/tactics/equality.ml

Lines 653 to 657 in 61ee398

	(tclFIRST
	[assumption;
	tclTHEN (apply sym) assumption;
	try_prove_eq
	])

I think when a tactic is explicitly given by by we shouldn't try assumption, (ie replace x with y tries assumption but replace x with y by tac doesn't).

Ot maybe we shouldn't try assumption at all but that would be more likely to break scripts in the wild.

We can also avoid using first and use tclORELSE0 instead to avoid eating the error without changing behaviour.

[SkySkimmer]

BTW I don't get the "ltac call .. failed" message, I guess you have ltac backtrace in coqrc or some such thing