The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Nope, it is not unintended, and you are right that it should rather be documented. It was first used internally in the setoid_rewrite resolution to avoid nested resolutions on which one couldn't backtrack but it now has more applicability in the new engine where goal handling and backtracking can be more explicitly managed. I'm not super happy to have new names apply_noTC, refine_noTC and so on though (the e-variants too). Maybe a modifier like unshelve would be more suited.
Best,
-- Matthieu

Le mer. 27 juil. 2016 à 19:38, Jonathan Leivent <jonikelee AT gmail.com> a écrit :

On 07/27/2016 09:35 AM, Jonathan Leivent wrote:
> ... But, I didn't know about class_apply ....
>

Note that class_apply defined in Classes.Init, based on another
undocumented tactic autoapply.  If the comments are to be believed, the
intention is merely to have an apply that respects the
Transparent/Opaque hints in the db it is given.  So, it may be the case
that this behavior of class_apply that has it not inducing inference in
subgoals is an unintended side-effect.

-- Jonathan