The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> On 08/19/2016 03:13 PM, Ralf Jung wrote:
>> However, if "--list-dependencies-of" would take wildcards, like "iris.*"
>> that could work.. oh wait, no. That would also cover all the reexported
>> unused axioms from the standard library, right?
> 
> That was the kind of think I was thinking about. And no, I do not think
> you can access an stdlib axiom via iris qualified names.

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"?
I thought that's what you were referring to when you said that one can
still access non-exported names through their fully qualified name.

However, somehow, it must be clear in the .vo file whether a name is
defined here or whether it is just re-exported -- and then coqchk should
simply check everything that's defined in the modules it gets as
argument, but nothing that's just re-exported. Couldn't that work?

Kind regards,
Ralf