coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Where did SetoidAxioms go?

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Daniil Frumin <difrumin AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Where did SetoidAxioms go?
Date: Tue, 07 Jan 2014 17:24:45 +0100

On 07/01/2014 16:59, Daniil Frumin wrote:
> It has disappeared in V8.3 and I didn't find the mention of it in the
> changelog
> and the last commit that removes it is
> 3b5e12a2eb98b34cacc1850f63b702dfea26cd57
>
> In particular I am looking for setoid_extensionality.

Wasn't that an inconsistent axiom? I think I remember it stated
something plain wrong. Can you remind us its type?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Where did SetoidAxioms go?, Daniil Frumin, 01/07/2014
- Re: [Coq-Club] Where did SetoidAxioms go?, Pierre-Marie Pédrot, 01/07/2014
  - Re: [Coq-Club] Where did SetoidAxioms go?, Daniil Frumin, 01/07/2014
    - Re: [Coq-Club] Where did SetoidAxioms go?, Arnaud Spiwack, 01/07/2014
      - Re: [Coq-Club] Where did SetoidAxioms go?, Daniil Frumin, 01/07/2014
        
        [Coq-Club] Where did SetoidAxioms go?, Matthieu Sozeau, 01/07/2014