Merge PR #12537: Take into account the existing delta-resolver when starting a new interactive module or module type

Reviewed-by: SkySkimmer

2 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 317e9c3757..09feca71e7 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -455,3 +455,6 @@ PreOrder_Reflexive:
 reflexive_eq_dom_reflexive:
   forall {A B : Type} {R' : Relation_Definitions.relation B},
   Reflexive R' -> Reflexive (eq ==> R')%signature
+B.b: B.a
+A.b: A.a
+F.L: F.P 0
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 4ec7a760b9..a5ac2cb511 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -66,3 +66,26 @@ Reset Initial.
 Require Import Morphisms.
 
 Search is:Instance [ Reflexive | Symmetric ].
+
+Module Bug12525.
+  (* This was revealing a kernel bug with delta-resolution *)
+  Module A. Axiom a:Prop. Axiom b:a. End A.
+  Module B. Include A. End B.
+  Module M.
+    Search B.a.
+  End M.
+End Bug12525.
+
+From Coq Require Lia.
+
+Module Bug12647.
+  (* Similar to #12525 *)
+  Module Type Foo.
+  Axiom P : nat -> Prop.
+  Axiom L : P 0.
+  End Foo.
+
+  Module Bar (F : Foo).
+  Search F.P.
+  End Bar.
+End Bug12647.