The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/28/2015 03:37 PM, Evelyne Contejean wrote:
> There is also the "ergo" tactic, due to Stéphane Lescuyer, as a part 
> of his thesis when he was a PhD student of mine.
>
> www.lix.polytechnique.fr/coq/pylons/.../Ergo/v8.3

I get a "404 Not Found" error for that link.

> This tactic is based on the SMT solver Alt-Ergo developed by me and 
> Sylvain Conchon.
>
> Regards,
>
> Évelyne Contejean