2 files changed, 10 insertions, 0 deletions
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.