The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/04/2014 22:35, Jonathan wrote:
> Is that true?  If not, how does one coerce automation like eauto to
> attempt such alternate subgoal solutions?  Or, if it is true, is there
> something else in the tactic language that can be used to drive such
> alternative-solution attempts when existential variables are present?

Well, you're right. Eauto does not really backtrack on evar instances.
This is for historical reasons, as the old tactic engine was not able to
do it properly. Some tactics (namely the typeclass-variant of eauto if
I'm not mistaken) had to be handwritten to do so.

Still, in the current trunk, there is a whole new engine which treats
evar instanciation and backtracking correctly, so that we could imagine
to have a nicer eauto. The problem is that there is a huge quantity of
legacy code which needs to be ported to the new engine, requiring a lot
of manpower in this process, precisely what we're lacking of. If you
need some given primitives, you can add them using ML code...

PMP

PMP

Attachment: signature.asc
Description: OpenPGP digital signature