Print Assumptions spuriously reports axioms from module types defined in another file

[jtassarotti]

Version 8.8.1

Operating system: Linux

Description of the problem

Define the following in a file "test.v":

Module Type A.
  Axiom f : True.
End A.

Module M : A.
  Lemma f : True. trivial. Qed. 
End M.

Then, if we have in another file

Require Import test.

Lemma test : True.
Proof. apply M.f. Qed.

Module N : A.
  Lemma f : True. trivial. Qed. 
End N.

Lemma test2 : True.
Proof. apply N.f. Qed.

Print Assumptions test.
Print Assumptions test2.

The first print assumption command claims there's an axiom:

Axioms:
M.f : True

while the second properly reports that the term is closed under the global context. Under 8.8.0, both are reported as closed. This is causing lots of spurious assumptions to be listed in my developments that use mathcomp libraries.

[ejgallego]

Confirmed on master.

[herbelin]

This was introduced in 1522b98 (my bad) which itself was conversely fixing a problem with missing constraints. See a fix at #8417.