Autogeneration of transitivity lemma preempts setoid even when it fails

[yannl35133]

See code at

rocq/tactics/tactics.ml

Lines 3189 to 3194 in 4d0c0bb

	| None,eq,eq_kind ->
	match t with
	| None ->
	let info = Exninfo.reify () in
	Tacticals.tclZEROMSG ~info (str"etransitivity not supported for this relation.")
	| Some t -> prove_transitivity eq eq_kind t

The hook for setoid is triggered by exception NoEquationFound, but when a conclusion fitting equality is found, etransitivity lemma is not generated and the command fails.

Minimal reproducer:

Require RelationClasses.

Module Control.

Inductive eq {A : Type} (x : A) : A -> Prop :=
| eq_refl : eq x x
| eq_no (f : False) y : eq x y
.

Instance eq_trans [A : Type] : RelationClasses.Transitive (@eq A).
Proof. now intros x y z e []. Defined.

Goal eq 0 1.
Proof. etransitivity.
Abort.

End Control.

Inductive eq {A : Type} (x : A) : A -> Prop :=
| eq_refl : eq x x
.

Instance eq_trans [A : Type] : RelationClasses.Transitive (@eq A).
Proof. now intros x y z e []. Defined.

Goal eq 0 1.
Proof. etransitivity. (* etransitivity not supported for this relation. *)
Abort.