The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I'm not sure you would learn much by digging up my commits as Pierre-Marie suggests. But the bottom-line is that the proof given to a goal has always been a regular Coq term but the interactive proof mechanism was built in a way which made it unable to retrieve such a proof. I wrote a completely new mechanism which, among other things, support the feature you need (it's often called dependent subgoals). This new implementation was already partially part of the v8.4, but it's been only completed in v8.5.

On 20 January 2015 at 15:15, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 20/01/2015 14:59, Soegtrop, Michael wrote:
> quite intriguing! So if I got you right, in 8.4 I cannot access the
> value of a tactic generated term inside a proof, only its type? This is
> unexpected since I can access the value after the proof is finished, if
> I end it with Defined rather than Qed. I wonder what makes it impossible
> to access it inside of the proof.

Short answer: the legacy proof engine.
Long answer: get a look at the merging of the branch of Arnaud in the
git repo.

> 1.       switch to 8.5 and try to fix ssreflect
>
> 2.       switch to 8.5 and try to port the ssreflect libraries I want to
> mainstream Coq
>
> 3.       stay with 8.4

If I am not mistaken, there is a 8.5-compatible version of ssreflect
already. We use it for testing. I do not know where it is officially
downloadable, but you should find it in the coq-contribs repo at least.

PMP