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

Reviewed-by: SkySkimmer

1 files changed, 10 insertions, 1 deletions

diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 9de8d6fbc3..f3b21eb813 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -53,7 +53,16 @@ let kind_searcher = Decls.(function
 let interp_search_item env sigma =
   function
   | SearchSubPattern ((where,head),pat) ->
-      let _,pat = Constrintern.intern_constr_pattern env sigma pat in
+      let expected_type = Pretyping.(if head then IsType else WithoutTypeConstraint) in
+      let pat =
+        try Constrintern.interp_constr_pattern env sigma ~expected_type pat
+        with e when CErrors.noncritical e ->
+          (* We cannot ensure (yet?) that a typable pattern will
+             actually be typed, consider e.g. (forall A, A -> A /\ A)
+             which fails, not seeing that A can be Prop; so we use an
+             untyped pattern as a fallback (i.e w/o no insertion of
+             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 ->
       GlobSearchString s