The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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