coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A smarter "induction;econstructor" combo?

From: Paolo Herms <paolo.herms AT cea.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A smarter "induction;econstructor" combo?
Date: Tue, 22 May 2012 17:36:58 +0200

On Tuesday 22 May 2012 15:19:10 Francois Pottier wrote:
> > econstuctor (solve [eauto]).
> > I don't think it's documented; I've found it by idly reading the Coq
> > source
> > code.
>
> !!

Of course, this is documented as part of the tactic language
http://coq.inria.fr/refman/Reference-Manual012.html
--
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France

[Coq-Club] A smarter "induction;econstructor" combo?, Francois Pottier, 05/21/2012
- Re: [Coq-Club] A smarter "induction;econstructor" combo?, Viktor Vafeiadis, 05/21/2012
- Message not available
  - Re: [Coq-Club] A smarter "induction;econstructor" combo?, Francois Pottier, 05/22/2012
    - Re: [Coq-Club] A smarter "induction;econstructor" combo?, Paolo Herms, 05/22/2012
      - Re: [Coq-Club] A smarter "induction;econstructor" combo?, AUGER Cédric, 05/22/2012
      - Re: [Coq-Club] A smarter "induction;econstructor" combo?, Pierre Courtieu, 05/23/2012
        
        Re: [Coq-Club] A smarter "induction;econstructor" combo?, Paolo Herms, 05/23/2012