From c68e580377c49435f50f08544c6e9c135f1783a6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 17 Jun 2020 17:47:03 +0200
Subject: Adding test for #12525 (Search of lemmas in Include failing when in
 Module).

---
 test-suite/output/Search.out |  3 +++
 test-suite/output/Search.v   | 23 +++++++++++++++++++++++
 2 files changed, 26 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3