The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/17/2014 06:12 PM, Pierre-Marie Pédrot wrote:
> 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

Thanks for the response.  I did see the new "+" backtracking branching 
operator in the trunk, but haven't tried it yet.  Does that allow 
backtracking over solved subgoals in order to alleviate this problem 
with evars?  Also, I didn't notice the typeclass-variant of eauto in the 
truck - where is that?

About the legacy code porting problem - are you implying that all Coq 
users will eventually be impacted by a change in eauto itself, or is the 
"legacy code" you're referring to instead Coq implementation code that 
will need conversion?

I have never tried writing ML primitives for Coq.  I do recall seeing 
some small amount of documentation on how to do that somewhere - I don't 
recall where.  Do you know where that documentation is?

Sorry for asking so many questions!  And thanks again.
-- Jonathan