The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  this is indeed supported and I'm documenting it right now, thanks

for the reminder! This works for typeclasses eauto only currently, hopefully it will 

be available for the other auto/eauto variants once we merge them.

Best regards,

-- Matthieu

On Wed, Nov 4, 2015 at 8:31 AM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi all,

> what is the status of the command:
>
>   Hint Cut
>
> that allows one to constraint (e)auto and type class instance search?
>
> It has been introduced by commit 1011266b in November 2011, but has
> never been documented, nor mentioned in any Changelog.
[snip]
> I would like to try to make use of this feature, but since it has not
> been documented or mentioned anywhere, I am not sure what will happen
> with it in the future.

We'd really like to rely on "Hint Cut" to make our typeclass setup
scale. But right now, we kind of fear that it may, one day, disappear
just as silently as it appeared four years ago - so some kind of
confirmation by the Coq devs, that this is a feature that's considered
"officially supported" and won't be just tossed away, would be very much
appreciated.

Kind regards,
Ralf