Merge branch 'v8.6'

3 files changed, 16 insertions, 10 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 93c3179bcf..5d1964a0ab 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -164,14 +164,17 @@ module Make
     | ModeNoHeadEvar -> str"!"
     | ModeOutput -> str"-"
 
+  let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+    pr_opt (fun x -> str"|" ++ int x) pri ++
+    pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
   let pr_hints db h pr_c pr_pat =
     let opth = pr_opt_hintbases db  in
     let pph =
       match h with
         | HintsResolve l ->
           keyword "Resolve " ++ prlist_with_sep sep
-            (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++
-              match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+            (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
             l
         | HintsImmediate l ->
           keyword "Immediate" ++ spc() ++
@@ -886,7 +889,7 @@ module Make
               spc() ++ pr_class_rawexpr c2)
         )
 
-      | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
+      | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
         return (
           hov 1 (
             (if abst then keyword "Declare" ++ spc () else mt ()) ++
@@ -897,7 +900,7 @@ module Make
               pr_and_type_binders_arg sup ++
               str":" ++ spc () ++
               (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
-              pr_constr cl ++ pr_priority pri ++
+              pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
               (match props with
                 | Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
                 | Some (true,_) -> assert false
@@ -911,11 +914,14 @@ module Make
             keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
         )
 
-      | VernacDeclareInstances (ids, pri) ->
-        return (
+      | VernacDeclareInstances insts ->
+         let pr_inst (id, info) =
+           pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+         in
+         return (
           hov 1 (keyword "Existing" ++ spc () ++
-                   keyword(String.plural (List.length ids) "Instance") ++
-                   spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
+                   keyword(String.plural (List.length insts) "Instance") ++
+                 spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
         )
 
       | VernacDeclareClass id ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b19f8376c0..8fabb70536 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -872,7 +872,7 @@ let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
   print_ref false (instance_impl i) ++
-  begin match instance_priority i with
+  begin match hint_priority i with
   | None -> mt ()
   | Some i -> spc () ++ str "|" ++ spc () ++ int i
   end
diff --git a/printing/printer.ml b/printing/printer.ml
index 3c8ad4255c..bfc2e1bc93 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -531,7 +531,7 @@ let print_evar_constraints gl sigma =
         str" with candidates:" ++ fnl () ++ hov 0 ppcandidates
     else mt ()
 
-let should_print_dependent_evars = ref true
+let should_print_dependent_evars = ref false
 
 let _ =
   let open Goptions in