1 files changed, 6 insertions, 8 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7ce2dd64af..989a6c5bf1 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -24,7 +24,6 @@ open Ltac_plugin
 open Notation_ops
 open Notation_term
 open Glob_term
-open Globnames
 open Stdarg
 open Genarg
 open Decl_kinds
@@ -218,8 +217,8 @@ let interp_search_notation ?loc tag okey =
          (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
       else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
     loop 0 1 in
-  let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in
-  let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in
+  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
   let pr_and_list pr = function
     | [x] -> pr x
     | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
@@ -294,7 +293,7 @@ let interp_search_notation ?loc tag okey =
     let scs' = List.remove (=) sc !scs in
     let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
     Feedback.msg_warning (hov 4 w)
-  else if String.string_contains ~where:ntn ~what:" .. " then
+  else if String.string_contains ~where:(snd ntn) ~what:" .. " then
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
@@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat =
       true, cp
     with _ -> false, [] in
   let coerce hp coe_index =
-    let coe = Classops.get_coercion_value coe_index in
+    let coe_ref = coe_index.Classops.coe_value in
     try
-      let coe_ref = global_of_constr coe in
       let n_imps = Option.get (Classops.hide_coercion coe_ref) in
       mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
-    with _ ->
-    errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
+    with Not_found | Option.IsNone ->
+    errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
             ++ str "to interpret head search pattern as type") in
   filter_head, List.fold_left coerce hpat' coe_path