Merge PR #18910: Set some basic rewriting primitives in Type opaque f…

…or TC search.

Reviewed-by: SkySkimmer
Ack-by: olaure01
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/11-standard-library/18910-setoid-type-core-tc-opaque.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  ``Coq.CRelationClasses.arrow``, ``Coq.CRelationClasses.iffT`` and
+  ``Coq.CRelationClasses.flip`` are now :cmd:`Typeclasses Opaque`
+  (`#18910 <https://github.com/coq/coq/pull/18910>`_,
+  by Pierre-Marie Pédrot).

test-suite/bugs/bug_7675_3.v

@@ -58,19 +58,15 @@ Ltac test S b1 b2 b3 b4 :=
     unfold arrow, Basics.arrow; now rewrite <- HR | clear Ht ].
 
 Goal True.
-test Ri   true  true  true  true.
+Proof.
 test Ra   true  true  true  true.
 test Rb   false false false false.
-test RBi  true  true  true  true.
 test RBa  true  true  true  true.
 test RBb  false false false false.
-test RTi  true  true  true  true.
 test RTa  true  true  true  true.
 test RTb  false false false false.
-test RRBi true  true  true  true.
 test RRBa true  true  true  true.
 test RRBb false false false false.
-test RRTi true  true  true  true.
 test RRTa true  true  true  true.
 test RRTb false false false false.
 apply I.

theories/Classes/CRelationClasses.v

@@ -33,6 +33,8 @@ Definition flip {A B C : Type} (f : A -> B -> C) := fun x y => f y x.
 
 Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type.
 
+Global Typeclasses Opaque flip arrow iffT.
+
 (** We allow to unfold the [crelation] definition while doing morphism search. *)
 
 Section Defs.