The Coq mailing list

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

I have a couple of declarations which produce existentials.  These
existentials are not instantiated as a side effect of discharging all of
the obligations of the declaration.

One way of dealing wiht this situation is to add an explicit term
instantiation at the end of the script:

   Lemma foo : bar.
     tactic.
     tactic.
     tactic.
     (* solved all obligations *)
     Existential 1:=term.
     Qed.

However, I want to build "term" using tactics rather than by explicitly
typing in a term.  The term is quite large and is essentially
proof-irrelevant (although it's in [Type] rather than [Prop] for
technical reasons) so I don't care about the structure of the term --
it's just a witness.

Is there any way for a proof which finishes with just one existential
left to turn that existential into a new subgoal which can be
instantiated with tactics?

Thanks,

  - a