From 1522b9899b669f4fdd0fc9be1963c5e96d81a13f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 7 Apr 2018 18:43:40 +0200
Subject: Fixes #7192 (Print Assumptions does not enter implementation of
 submodules).

We fix it by looking manually for the implementation at each level of
nesting rather than using the signature for the n first levels and
looking for the implementation only in the n+1-th level.
---
 test-suite/output/PrintAssumptions.out |  2 ++
 test-suite/output/PrintAssumptions.v   | 27 +++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 66458543a..34f44cd24 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -18,3 +18,5 @@ Closed under the global context
 Closed under the global context
 Axioms:
 M.foo : False
+Closed under the global context
+Closed under the global context
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.
-- 
cgit v1.2.3