The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2015 11:25 AM, Jonathan Leivent wrote:
> ...
> Goal True.
> assert (True \/ False \/ True) as P1 by tauto.
> assert (True \/ True \/ False) as P2 by tauto.
> assert (False \/ False \/ True) as P3 by tauto.
> assert (True \/ False \/ False) as P4 by tauto.
> Fail shape (xsh x y, x \/ x \/ y)
>   ltac:(fun H X => hypntype H; idtac X; let Y:=nthxsh 1 X in idtac Y); 
> fail.
> repeat shape (xsh x y, x \/ x \/ y)
>   ltac:(fun H X => hypntype H; clear H; let Y:=nthxsh 0 X in idtac Y).
>
> -- Jonathan

Oops - sorry.  That "hypntype" tactic is just:

Ltac hypntype H := let t:=type of H in idtac H ":" t.