The Coq mailing list

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

On 18/04/2014 01:10, Jonathan wrote:
> 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?

Yes, this + operator combined with the semicolon should backtrack
correctly over evars.

> Also, I didn't notice the typeclass-variant of eauto in the truck -
> where is that?

It's not only in the trunk, it has been here for some time as far as I
know. Blaming the repo gives me around October 2009. The tactic itself
seems undocumented, but you can use it as follows:

typeclasses eauto
typeclasses eauto using db1 ... dbn

The first version will use the typeclass database and will only try to
solve class instances, while the second one is the « good » eauto you're
searching for, with the provided hint databases.

> 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?

The latter one, though changing eauto's behaviour may impact quite a lot
of users. Backward compatibility, blah blah.

> 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?

There is a tutorial by Thomas Braibant on github.

https://github.com/braibant/coq-tutorial-ml-tactics

It has to be adapted to the trunk version of Coq, but the main lines are
the same, only the API changed so you can look at the .mli files of Coq
to give you an idea (or send a mail to this list).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature