aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/PrintAssumptions.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/PrintAssumptions.v')
-rw-r--r--test-suite/output/PrintAssumptions.v27
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index c2003816c..ea1ab6378 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -110,3 +110,30 @@ End N.
Print Assumptions N.foo.
End INCLUDE.
+
+(* Print Assumptions did not enter implementation of submodules (#7192) *)
+
+Module SUBMODULES.
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module E: C.
+ Module D <: B. Definition f := a. End D.
+End E.
+Print Assumptions E.D.f.
+
+(* Idem in the scope of a functor *)
+
+Module Type T. End T.
+Module F (X : T).
+ Definition a := True.
+ Module Type B. Axiom f : Prop. End B.
+ Module Type C. Declare Module D : B. End C.
+ Module E: C.
+ Module D <: B. Definition f := a. End D.
+ End E.
+ Print Assumptions E.D.f.
+End F.
+
+End SUBMODULES.