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.