The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Thu, Apr 07, 2011 at 11:37:36AM +0200, Chantal Keller wrote:
> 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.

I know it, but, sometimes, [inversion_clear] does not work properly: I
have a case when it forgets some generated hypotheses, preventing
to complete the proof.

In that case, it worked only with [inversion] followed by [subst].

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