Typing patterns and using type constraints in Search.

We accept patterns that we failed to type as a fallback.

6 files changed, 34 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7dbc6c86a6..efab586f8a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2472,8 +2472,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
   pattern_of_glob_constr c
 
 let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
-  let kind_for_intern = match expected_type with OfType _ -> WithoutTypeConstraint | _ -> expected_type in
-  let c = intern_gen kind_for_intern ~pattern_mode:true env sigma c in
+  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
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 09feca71e7..503cfa2732 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