coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Megacz <megacz AT cs.berkeley.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Re: apply to all subgoals?
- Date: Sun, 26 Sep 2010 20:25:59 +0000
- Cancel-lock: sha1:S6myH3IbZJc21hFhmfgL5Gq38SQ=
- Organization: Myself
Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>
writes:
> I'm not sure I understood your problem exactly, but maybe one of the
> things here might help you:
> http://coq.inria.fr/refman/Reference-Manual028.html#toc143
Alexandre, thanks for your reply. What you point to is the same thing I
mentioned here:
>> I suppose I could also use [Program Instance] and [Solve All Obligations
>> using];
I was hoping for a solution which could be used in normal [Instance] and
[Definition] clauses, just like "5:<tactic>" can. I've had some issues
recently with [Program] insisting that I import the JMeq axioms, which
is something I do not want to do.
But thanks anyways!
- a
- [Coq-Club] apply to all subgoals?, Adam Megacz
- Re: [Coq-Club] apply to all subgoals?,
Alexandre Pilkiewicz
- [Coq-Club] Re: apply to all subgoals?, Adam Megacz
- Re: [Coq-Club] apply to all subgoals?,
Alexandre Pilkiewicz
Archive powered by MhonArc 2.6.16.