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

Reviewed-by: SkySkimmer

8 files changed, 54 insertions, 1 deletions

diff --git a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst
new file mode 100644
index 0000000000..03be92f897
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Added support for automatic insertion of coercions in :cmd:`Search`
+  patterns. Additionally, head patterns are now automatically
+  interpreted as types
+  (`#13255 <https://github.com/coq/coq/pull/13255>`_,
+  fixes `#13244 <https://github.com/coq/coq/issues/13244>`_,
+  by Hugo Herbelin).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 409e46864e..ecf2b951a2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2518,6 +2518,14 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
             ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
+let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
+  let c = intern_gen expected_type ~pattern_mode:true env sigma c in
+  let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
+  let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
+  (* FIXME: it is necessary to be unsafe here because of the way we handle
+     evars in the pretyper. Sometimes they get solved eagerly. *)
+  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
+
 let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
   let tmp_scope = scope_of_type_kind env sigma kind in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 898a3e09c8..11d756803f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -136,10 +136,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
 
 (** Interprets constr patterns *)
 
+(** Without typing *)
 val intern_constr_pattern :
   env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
+(** With typing *)
+val interp_constr_pattern :
+  env -> evar_map -> ?expected_type:typing_constraint ->
+    constr_pattern_expr -> constr_pattern
+
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
 val intern_reference : qualid -> GlobRef.t
 
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 914e7f88c6..ef4c6bac93 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:(~~ _).
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