coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Destruct vs. inversion

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Destruct vs. inversion
Date: Thu, 07 Apr 2011 11:37:17 +0200

Hi,

Le 06/04/2011 19:42, Daniel de Rauglaudre a écrit :

There is another reason why I don't like inversion: it often generates
a lot of unuseful sub-variables, I don't know why. I often write:
inversion x; subst.

You might be interested in the [inversion_clear] tactic.
--
Chantal KELLER

[Coq-Club] Destruct vs. inversion, Benjamin C. Pierce
- Re: [Coq-Club] Destruct vs. inversion, Daniel Schepler
- Re: [Coq-Club] Destruct vs. inversion, Nathan Collins
- Re: [Coq-Club] Destruct vs. inversion, Guillaume Melquiond
  - Re: [Coq-Club] Destruct vs. inversion, Jean-Francois Monin
  - Re: [Coq-Club] Destruct vs. inversion, Benjamin C. Pierce
    - Re: [Coq-Club] Destruct vs. inversion, Jacques Garrigue
    - Message not available
      - Re: [Coq-Club] Destruct vs. inversion, Pierre Boutillier
- Message not available
  - Re: [Coq-Club] Destruct vs. inversion, Paolo Herms
- <Possible follow-ups>
- Re: [Coq-Club] Destruct vs. inversion, Daniel de Rauglaudre
  - Re: [Coq-Club] Destruct vs. inversion, Chantal Keller
  - Message not available
    - Re: [Coq-Club] Destruct vs. inversion, Daniel de Rauglaudre