coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"
Date: Tue, 20 Jan 2015 15:15:36 +0100

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

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
- Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
  - RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
    - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Pierre-Marie Pédrot, 01/20/2015
      - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Georges Gonthier, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/21/2015
        
        Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Enrico Tassi, 01/21/2015