The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Indeed there was a proposal recently to remove axioms from the usual Require Import Program, but

that in turn will force anyone who uses dependent destruction to explicitly Require Import Program.Equality.

It's only Program.Tactics and Program.Wf that are necessary for Program to function correctly (IIRC, for 

the default program_simpl tactic and well-founded fixpoint combinators).

-- Matthieu

On Fri, Aug 19, 2016 at 3:47 PM Ralf Jung <jung AT mpi-sws.org> wrote:

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