coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Francois Pottier <Francois.Pottier AT inria.fr>
To: Viktor Vafeiadis <viktor AT mpi-sws.org>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A smarter "induction;econstructor" combo?
Date: Tue, 22 May 2012 15:19:02 +0200

Dear Viktor,

On Mon, May 21, 2012 at 07:35:41PM +0200, Viktor Vafeiadis wrote:
> You can try:
> econstuctor (solve [eauto]).

This is extremely cool. It seems to work, indeed. Thanks!

> I don't think it's documented; I've found it by idly reading the Coq source
> code.

!!

--
François Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/

[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