The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Alexandre Pilkiewicz wrote:
> > You can build a list of candidate hypotheses by getting each hypothesis out
> > of the way as you first select it.  For instance, run [generalize dependent
> > H] inside your loop, and then [intros] all the hypotheses back into place
> > afterward, once you've built a list of hypotheses (say, as a tuple).
> >      
> I don't understand how to build a list of hypotheses, but the
> generalize dependent does the trick!
>
> Thanks
>
> - Alexandre Pilkiewicz
>    

Here's some code to build a list of all hypothesis conclusions.  (It 
will probably act strangely if some hypothesis has a type dependent on 
another hypothesis.)

Require Import List.

Ltac everyone k :=
  let rec f acc :=
    match goal with
      | [ H : ?T |- _ ] => generalize dependent H; f (@cons Type T acc)
      | _ => k acc
    end in
    f (@nil Type).

Goal forall x y z : nat, x = y -> y = z -> x = z.
  intros; everyone ltac:(fun x => pose x).