Skip to content

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

Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:notc-search into master

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 be fixed, this can be
deprecated or replaced by the new syntax. *)

Rationale for inclusion

I think 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 onwards.

Edited by Robbert Krebbers

Merge request reports