coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 15:51:57 +0200

On 19/08/2016 15:46, Ralf Jung wrote:

> Isn't it the case that if I say in iris/prelude/base.v
>
> Require Import Setoid
>
> then I can later access "iris.prelude.Setoid"?

No (assuming you are talking about Coq.Setoids.Setoid here).

Best regards,

Guillaume

[Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Matthieu Sozeau, 08/19/2016
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        Re: [Coq-Club] Axioms reported by coqchk, Pierre-Marie Pédrot, 08/19/2016
        
        RE: [Coq-Club] Axioms reported by coqchk, Soegtrop, Michael, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/19/2016