Add a way to disable typeclass search in `Program` obligations

From the coqdoc of the new feature:

(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Proper] obligations.
Should https://github.com/coq/coq/issues/12147 be fixed, this can be
deprecated or replaced by the new syntax. *)

Rationale for inclusion

I think https://github.com/coq/coq/issues/12147 is potentially bad enough that it could belong in stdpp. I haven't found very compelling usecases in iris: in part, you already avoid writing Program Definition foo ...: A -n> B, at the cost of more boilerplate.

See also: discussion from https://mattermost.mpi-sws.org/iris/pl/r885z6apefr9bjpuctczruogrr onwards.

theories/base.v

@@ -89,6 +89,14 @@ Definition tc_opaque {A} (x : A) : A := x.
 Typeclasses Opaque tc_opaque.
 Arguments tc_opaque {_} _ /.
 
+(** When using [Program], you can use [notc_hole] in place of [_] to create
+an obligation that does not trigger typeclass search. That is useful if the
+search fails slowly, for instance for [Proper] obligations.
+Should https://github.com/coq/coq/issues/12147 be fixed, this can be
+deprecated or replaced by the new syntax. *)
+Definition disable_tc_search {T : Type} (x : id T) : T := x.
+Notation notc_hole := (disable_tc_search _).
+
 (** Below we define type class versions of the common logical operators. It is
 important to note that we duplicate the definitions, and do not declare the
 existing logical operators as type classes. That is, we do not say: