coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Applying an axiom to all hypotheses in context at once

From: Adam Chlipala <adamc AT hcoop.net>
To: Marko Malikovi� <marko AT ffri.hr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Applying an axiom to all hypotheses in context at once
Date: Fri, 03 Jul 2009 08:57:22 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Marko Malikovi� wrote:

assume that we have context:

H : _
H0 : _
H1 : _
...
Hn : _
-----------------
Goal

and an axiom A.

I'm searching for a simply way to apply axiom A in all hypotheses H, H0,
H1, ... , Hn at once.

I'm not entirely sure what you have in mind, but maybe this is what you want:

repeat match goal with [ H : _ |- _ ] => apply A in H end

[Coq-Club] Applying an axiom to all hypotheses in context at once, Marko Malikovi�
- Re: [Coq-Club] Applying an axiom to all hypotheses in context at once, Adam Chlipala
  - Re: [Coq-Club] Applying an axiom to all hypotheses in context at once, Marko Malikovi�