Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, not only on subidentifiers of an identifier

Reviewed-by: Zimmi48

6 files changed, 25 insertions, 1 deletions

diff --git a/doc/changelog/07-commands-and-options/13351-master+search-all-subparts-ident.rst b/doc/changelog/07-commands-and-options/13351-master+search-all-subparts-ident.rst
new file mode 100644
index 0000000000..f3ad6dcaca
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13351-master+search-all-subparts-ident.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  :cmd:`Search` supports filtering on parts of identifiers which are
+  not proper identifiers themselves, such as :n:`"1"`
+  (`#13351 <https://github.com/coq/coq/pull/13351>`_,
+  fixes `#13349 <https://github.com/coq/coq/issues/13349>`_,
+  by Hugo Herbelin).
diff --git a/kernel/names.ml b/kernel/names.ml
index 5b6064fa9f..13761ca245 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -44,6 +44,10 @@ struct
   | None -> true
   | Some _ -> false
 
+  let is_valid_ident_part s = match Unicode.ident_refutation ("x"^s) with
+  | None -> true
+  | Some _ -> false
+
   let of_bytes s =
     let s = Bytes.to_string s in
     check_valid s;
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a4ceef802..74a4e6f7d0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -44,6 +44,9 @@ sig
   val is_valid : string -> bool
   (** Check that a string may be converted to an identifier. *)
 
+  val is_valid_ident_part : string -> bool
+  (** Check that a string is a valid part of an identifier *)
+
   val of_bytes : bytes -> t
   val of_string : string -> t
   (** Converts a string into an identifier.
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.
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index f3b21eb813..af51f4fafb 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -64,7 +64,8 @@ let interp_search_item env sigma =
              coercions, no compilation of pattern-matching) *)
           snd (Constrintern.intern_constr_pattern env sigma ~as_type:head pat) in
       GlobSearchSubPattern (where,head,pat)
-  | SearchString ((Anywhere,false),s,None) when Id.is_valid s ->
+  | SearchString ((Anywhere,false),s,None)
+      when Id.is_valid_ident_part s && String.equal (String.drop_simple_quotes s) s ->
       GlobSearchString s
   | SearchString ((where,head),s,sc) ->
       (try