coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] SMT solvers for Coq?

From: David MENTRE <dmentre AT linux-france.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] SMT solvers for Coq?
Date: Wed, 29 Apr 2015 16:09:16 +0200

Hello,

Le 29/04/2015 15:53, Jonathan Leivent a écrit :

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.

Following URL is working (found with Google):

http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Ergo/v8.4/Ergo.tar.gz

Best regards,
david

[Coq-Club] SMT solvers for Coq?, Jonathan Leivent, 04/28/2015
- Re: [Coq-Club] SMT solvers for Coq?, Beta Ziliani, 04/28/2015
  - Re: [Coq-Club] SMT solvers for Coq?, Chantal Keller, 04/28/2015
    - Re: [Coq-Club] SMT solvers for Coq?, Evelyne Contejean, 04/28/2015
      - Re: [Coq-Club] SMT solvers for Coq?, Jonathan Leivent, 04/29/2015
        
        Re: [Coq-Club] SMT solvers for Coq?, David MENTRE, 04/29/2015
        
        Re: [Coq-Club] SMT solvers for Coq?, Jonathan Leivent, 04/29/2015
        
        Re: [Coq-Club] SMT solvers for Coq?, Frédéric Blanqui, 04/29/2015
        Re: [Coq-Club] SMT solvers for Coq?, Jonathan Leivent, 04/29/2015
        Re: [Coq-Club] SMT solvers for Coq?, Pierre-Yves Strub, 04/30/2015