From 696b97978668f7d145af98b4163d4f32352b7442 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 11 Nov 2020 16:24:45 +0100
Subject: Addressing #13349: accept Search on subparts of ident, not only on
 subidents.

---
 test-suite/output/Search.out | 4 ++++
 test-suite/output/Search.v   | 6 ++++++
 2 files changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index ef4c6bac93..0f5fd91d93 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -462,3 +462,7 @@ 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
+partition_cons1:
+  forall [A : Type] (f : A -> bool) (a : A) (l : list A) [l1 l2 : list A],
+  partition f l = (l1, l2) ->
+  f a = true -> partition f (a :: l) = (a :: l1, l2)
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 2f29e1aff1..3419d5ac62 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -96,3 +96,9 @@ Module WithCoercions.
   Axiom f : None = 0.
   Search (None = 0).
 End WithCoercions.
+
+Require Import List.
+
+Module Wish13349.
+Search partition "1" inside List.
+End Wish13349.
-- 
cgit v1.2.3