The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a good way to get [match goal with ... end] to respect the typing/naming of hypotheses?  That is, is there a variant of

    Goal forall (n m : nat) (n' m' : unit) (f : nat -> nat -> Type) (f' : unit -> unit -> Type) (P : nat -> Prop) (fn : P n -> f n m -> f' n' m'), False.

      intros.

      match goal with

        | [ H : unit -> unit -> _, H1 : appcontext[?H ?a ?b] |- _ ] => pose H

      end.

that gives me a new hypothesis [T := f' : unit -> unit -> Type] rather than [T := f : nat -> nat -> Type]?  (I know that I can match for the type of [H] after the fact, but this seems like it gets unwieldy quickly, if I have multiple hypotheses that I'm trying to match against simultaneously.)

Thanks.

-Jason