The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The problem has nothing to do with files or imports and everything to do with module functors.  Functors are generative: Every time you apply a module functor, you get a fresh copy of every definition.  In particular, the inductive types and axioms you get by applying a functor twice do not unify.  The solution is to move inductive type definitions (and axioms, if need be) outside of your functors.

On Tue, Aug 9, 2016, 7:03 PM John Wiegley <johnw AT newartisans.com> wrote:

Hello,

I have a project that I'd like to modularize more using module functors.  I
end up with a dependency tree similar to the following:

    A: defines "foo"

    B: imports A to use "foo"
    C: imports A to use "foo"

    D: imports both B and C

What happens is that I run into a situation in D where [B.foo] and [C.foo] are
not considered the same type.  I have attached an example below.  Is there any
way to tell Coq that the definitions imported by B and C from A are to be
regarded as the same?


Thanks,
--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2