From 2355b3ed9a9af853b67f406d61404c4c05f8c8e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 19:41:47 +0200
Subject: Typing patterns and using type constraints in Search.

We accept patterns that we failed to type as a fallback.
---
 test-suite/output/Search.out    | 4 ++++
 test-suite/output/Search.v      | 7 +++++++
 test-suite/output/bug_13244.out | 9 +++++++++
 test-suite/output/bug_13244.v   | 3 +++
 4 files changed, 23 insertions(+)
 create mode 100644 test-suite/output/bug_13244.out
 create mode 100644 test-suite/output/bug_13244.v

(limited to 'test-suite')

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 09feca71e7..503cfa2732 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:(~~ _).
-- 
cgit v1.2.3