coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] slicing along the statement of theorem

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: St�phane Glondu <steph AT glondu.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] slicing along the statement of theorem
Date: Fri, 13 Apr 2012 16:59:14 +0200

On 04/13/2012 12:02 PM, St�phane Glondu wrote:

> This can be done in a plugin. I've attached a proof of concept.

Looks great! Will try it ASAP on my real example (not Fermat's
proof...). Thanks a lot,

- Xavier

[Coq-Club] slicing along the statement of theorem, Xavier Leroy
- Re: [Coq-Club] slicing along the statement of theorem, Randy Pollack
- Re: [Coq-Club] slicing along the statement of theorem, St�phane Glondu
  - Re: [Coq-Club] slicing along the statement of theorem, Makarius
    - History of backward application |> [Re: [Coq-Club] slicing along the statement of theorem], Andreas Abel
    - Re: [Coq-Club] slicing along the statement of theorem, Erik Ernst
      - Re: [Coq-Club] slicing along the statement of theorem, Makarius
  - Re: [Coq-Club] slicing along the statement of theorem, Xavier Leroy