coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unblocked, thanks!

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: Jean-Francois Monin <jean-francois.monin AT imag.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] unblocked, thanks!
Date: Mon, 13 Dec 2010 14:20:51 +0100

Hi,

On Mon, Dec 13, 2010 at 11:56:26AM +0100, Jean-Francois Monin wrote:

> Yes. A recent and convenient tactic to get the same effect is revert.
> Something like
> intros a b; revert a; induction b etc.

Noticed. Thanks.

> Forgot to explain fix 2 : it is an undocumented tactic
> [...]
> You have to know what you are doing, and some tactics like auto
> become dangerous. [...]

I indeed experimented that. It copied my conclusion into the hypotheses!
No surprised that "assumption" worked, but Qed did not. Morality: I prefer
not touch "fix" now :-)

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Re: [Coq-Club] blocked in an elementary proof, Petar Maksimovic
- Re: [Coq-Club] blocked in an elementary proof, Martijn Vermaat
  - Re: [Coq-Club] blocked in an elementary proof, St�phane Lescuyer
  - Message not available
    - Re: [Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Message not available
  - Re: [Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Message not available
  - Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
    - Re: [Coq-Club] unblocked, thanks!, Jean-Francois Monin
    - Message not available
      - Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
        
        Re: [Coq-Club] unblocked, thanks!, Jean-Francois Monin
        
        Message not available
        
        Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
        
        Re: [Coq-Club] unblocked, thanks!, quentin . carbonneaux
        Re: [Coq-Club] unblocked, thanks!, AUGER Cedric