coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] About the declarative mode

From: Ian Lynagh <igloo AT earth.li>
To: AUGER Cedric <Cedric.Auger AT lri.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] About the declarative mode
Date: Tue, 7 Dec 2010 19:58:25 +0000

On Mon, Dec 06, 2010 at 06:11:45PM +0100, AUGER Cedric wrote:
>
> As often, it is very surprising that a 4 line proof in manual require
> so much lines in Cezar (but also in normal mode, if you do not use
> highly automated proofs).
>
> Is this mode "frozen" (with all these flaws) or is it not?

Czar appears to be unmaintained, sadly.

There is at least one show-stopper for me:
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2371

Thanks
Ian

[Coq-Club] Equations from match-case unifiers under refine tactic, Petter Urkedal
- Re: [Coq-Club] Equations from match-case unifiers under refine tactic, Adam Chlipala
  - Re: [Coq-Club] Equations from match-case unifiers under refine tactic, Petter Urkedal
    - [Coq-Club] About tactic inversion, AUGER Cedric
      - Re: [Coq-Club] About tactic inversion, gallais @ EnsL.org
      - [Coq-Club] About the declarative mode, AUGER Cedric
        
        Re: [Coq-Club] About the declarative mode, Ian Lynagh
        
        Re: [Coq-Club] About the declarative mode, Pierre Corbineau
      - Re: [Coq-Club] About tactic inversion, Matthieu Sozeau
        
        Re: [Coq-Club] About tactic inversion, AUGER Cedric