coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Structured proofs do not work inside sections

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Victor Porton <porton AT narod.ru>
Cc: Coq <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Structured proofs do not work inside sections
Date: Fri, 11 Nov 2011 17:28:38 -0500

A brief note, and someone should correct me if I'm wrong about this: I believe the user base of "structured proofs" in Coq is negligible. Few of us here have any experience with it or recommend using it.

[Coq-Club] Structured proofs do not work inside sections, Victor Porton
- Re: [Coq-Club] Structured proofs do not work inside sections, Adam Chlipala
  - Re: [Coq-Club] Structured proofs do not work inside sections, Alan Pogrebinschi
    - Re: [Coq-Club] Structured proofs do not work inside sections, Adam Chlipala
      - Re: [Coq-Club] Structured proofs do not work inside sections, Pierre Courtieu
        
        Re: [Coq-Club] Structured proofs do not work inside sections, Alexandre Pilkiewicz
        
        Re: [Coq-Club] Structured proofs do not work inside sections, Adam Chlipala
- Re: [Coq-Club] Structured proofs do not work inside sections, Benedikt Ahrens