Merge PR #13255: Fixes #13244: support for coercions in Search

Reviewed-by: SkySkimmer

4 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 914e7f88c6..ef4c6bac93 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -458,3 +458,7 @@ reflexive_eq_dom_reflexive:
 B.b: B.a
 A.b: A.a
 F.L: F.P 0
+inr: forall {A B : Type}, B -> A + B
+inl: forall {A B : Type}, A -> A + B
+(use "About" for full details on the implicit arguments of inl and inr)
+f: None = 0
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index a5ac2cb511..2f29e1aff1 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -89,3 +89,10 @@ Module Bug12647.
   Search F.P.
   End Bar.
 End Bug12647.
+
+Module WithCoercions.
+  Search headconcl:(_ + _) inside Datatypes.
+  Coercion Some_nat := @Some nat.
+  Axiom f : None = 0.
+  Search (None = 0).
+End WithCoercions.
diff --git a/test-suite/output/bug_13244.out b/test-suite/output/bug_13244.out
new file mode 100644
index 0000000000..8c7d4ac776
--- /dev/null
+++ b/test-suite/output/bug_13244.out
@@ -0,0 +1,9 @@
+negbT: forall [b : bool], b = false -> ~~ b
+contra_notN: forall [P : Prop] [b : bool], (b -> P) -> ~ P -> ~~ b
+contraPN: forall [P : Prop] [b : bool], (b -> ~ P) -> P -> ~~ b
+contraNN: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
+contraL: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
+contraTN: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
+contra: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
+introN: forall [P : Prop] [b : bool], reflect P b -> ~ P -> ~~ b
+contraFN: forall [c b : bool], (c -> b) -> b = false -> ~~ c
diff --git a/test-suite/output/bug_13244.v b/test-suite/output/bug_13244.v
new file mode 100644
index 0000000000..83eaac1a35
--- /dev/null
+++ b/test-suite/output/bug_13244.v
@@ -0,0 +1,3 @@
+Require Import ssr.ssrbool.
+Set Warnings "-ssr-search-moved".
+Search headconcl:(~~ _).