coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] latest Coq trunk breaks some things

From: Jonathan <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] latest Coq trunk breaks some things
Date: Tue, 06 May 2014 21:41:08 -0400

After doing a git pull of the trunk - which included a large number of changes around universe polymorphism (changes through 2014-05-06), proofs that were working previously are now failing. I don't think any of these proofs had much if anything to do with universe polymorphism.

I'll follow up with some test cases, which I'll first try to factor out of the surrounding code...

-- Jonathan

[Coq-Club] latest Coq trunk breaks some things, Jonathan, 05/07/2014
- Re: [Coq-Club] latest Coq trunk breaks some things, Jonathan, 05/07/2014
  - Re: [Coq-Club] latest Coq trunk breaks some things, Jonathan, 05/07/2014
    - Re: [Coq-Club] latest Coq trunk breaks some things, Matthieu Sozeau, 05/07/2014
      - Re: [Coq-Club] latest Coq trunk breaks some things, Jonathan, 05/07/2014
      - Message not available
        
        [Coq-Club] professional advice for a young Coq developer, Larry D. Lee jr., 05/22/2014
        
        Re: [Coq-Club] professional advice for a young Coq developer, Adam Chlipala, 05/23/2014
        
        Re: [Coq-Club] professional advice for a young Coq developer, Ramana Kumar, 05/23/2014
        
        Re: [Coq-Club] professional advice for a young Coq developer, David MENTRE, 05/23/2014
        Re: [Coq-Club] professional advice for a young Coq developer, Adam Chlipala, 05/23/2014
        Re: [Coq-Club] professional advice for a young Coq developer, Bas Spitters, 05/23/2014