coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about multiple imports of the same modules

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about multiple imports of the same modules
Date: Tue, 09 Aug 2016 19:03:01 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f53.google.com
Ironport-phdr: 9a23:GJbgGxWDASu8fqveMtEgQPiSJ+PV8LGtZVwlr6E/grcLSJyIuqrYZhGAt8tkgFKBZ4jH8fUM07OQ6PG5HzRaqsvZ+DBaKdoXBkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2asc272qiI9oHJZE0Q3XzmMOo0dE/98F2Z9pFPx9AzcuBpklqBi0ALUtwe/XlvK1OXkkS0zeaL17knzR5tvek8/dVLS6TwcvdwZ7VZCDM7LzJ9v5Wz5lGQBTeIs3AbSyAdlgdCKwnD9hDzGJnr4QXgse8okgudPcu+crE5VjCv/u0jHB3viCEYHzg072jNls1rhaRA5hmmokoskMbvfIiJOa8mLevmdtQASD8ZUw==
Organization: New Artisans LLC

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?

Attachment: A.v
Description: Binary data

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

[Coq-Club] Question about multiple imports of the same modules, John Wiegley, 08/10/2016
- Re: [Coq-Club] Question about multiple imports of the same modules, Jason Gross, 08/10/2016