Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: apply to all subgoals?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: apply to all subgoals?


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page