The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm working on a development trying to track down a universe inconsistency and I've run into difficulties tracking it down. I have a blank file and do:

Require Import foo.

Require Import bar.

Here I get a universe inconsistency when including bar.

So I include the text of foo verbatim and run it, I get a universe inconsistency. I included contents of foo to find the minimal amount that is necessary to retain the universe inconsistency. So now I have,

(* a bunch of stuff included from foo *)

Require Import bar. (* <<--- universe inconsistency here *)

Now I repeat the process on bar. But when I inline the contents of bar and evaluate it, Coq accepts all of the definitions without a universe inconsistency.

Is this expected behavior? Are there extra checks that are occuring when importing a file that are not processed when the definitions are done inline? Is there some reason why inlining should make universes consistent?

Thank you.

--

gregory malecha