The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

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