The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

using Jonathan's trick to mix Ltac and value returning functions, I came up 
with this Ltac function, which collects all hypothesis of a given type, 
clears the hypothesis and returns a list of the hypothesis.

Ltac CollectAndClearHypothesis T :=
  let rec f l :=
    lazymatch goal with 
      | H1 := ?h1 : T |- _ =>
          (* need to wrap the clear H1 in a match goal to mix it with 
returning a term *)
          let dummy := match goal with |- _ => clear H1 end in
          let l' := constr:(h1::l) in f l'
      | |- _ => l
    end
  in f (@nil T).

It is used like this:

  let l := CollectAndClearHypothesis PropWrap in idtac l.

Thanks Jonathan!

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928