Anomaly: unknown constant in Print Assumptions

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3948
From: @Lionel-Rieg
Reported version: trunk
CC: @ppedrot

[coqbot]

Comment author: @Lionel-Rieg

Created attachment 539
Test case

In the attached file, the [Print Assumptions] command triggers the following anomaly:
Anomaly: Print Assumption: unknown constant Coq.MSets.MSetAVL.X.t.
Please report.

Attached file: file_3948.txt (text/plain, 2424 bytes)
Description: Test case

[coqbot]

Comment author: @ppedrot

Here is a shorter example.

Require Import MSets.

Declare Module X : Orders.OrderedType.

Module Type Interface.
Parameter constant : unit.
End Interface.

Module DepMap : Interface.
Module Dom := MSetAVL.Make(X).
Definition constant : unit :=
let _ := Dom.fold in tt.
End DepMap.

Print Assumptions DepMap.constant.

[coqbot]

Comment author: @ppedrot

This one is even self-contained.

Module Type S.
Parameter t : Type.
End S.

Module Bar(X : S).
Proof.
Definition elt := X.t.
Axiom fold : elt.
End Bar.

Module Make (X: S) := Bar(X).

Declare Module X : S.

Module Type Interface.
Parameter constant : unit.
End Interface.

Module DepMap : Interface.
Module Dom := Make(X).
Definition constant : unit :=
let _ := @ Dom.fold in tt.
End DepMap.

Print Assumptions DepMap.constant.

[coqbot]

Comment author: @maximedenes

It was a tricky one :) Incorrect composition of module substitutions.
Fixed in v8.5 branch, thanks for reporting!