Merge pull request rocq-archive#421 from gares/quickfix

adapt to coq/coq#19147
proux01 · Jun 24, 2024 · 7563a3d · 7563a3d
2 parents eb845aa + 9a76455
commit 7563a3d
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/serapi/serapi_pp.ml b/serapi/serapi_pp.ml
@@ -72,7 +72,7 @@ let pp_feedback_content fmt fb =
   | Custom(_loc, msg, _xml) -> fprintf fmt "Custom: %s" msg
 
   (* Old generic messages *)
-  | Message(_lvl, _loc, m) -> fprintf fmt "Msg: @[%a@]" Pp.pp_with m
+  | Message(_lvl, _loc, _qf, m) -> fprintf fmt "Msg: @[%a@]" Pp.pp_with m
 
 let pp_feedback fmt (fb : Feedback.feedback) =
   let open Feedback in

diff --git a/sertop/sertop_util.ml b/sertop/sertop_util.ml
@@ -42,7 +42,7 @@ module F = Feedback
 let feedback_content_pos_filter txt (fbc : F.feedback_content) : F.feedback_content =
   let adjust _txt loc = loc in
   match (fbc : F.feedback_content) with
-  | F.Message (lvl,loc,msg) -> F.Message (lvl, adjust txt loc, msg)
+  | F.Message (lvl,loc,qf,msg) -> F.Message (lvl, adjust txt loc, qf, msg)
   | _                       -> fbc
 
 let feedback_pos_filter text (fb : F.feedback) : F.feedback =
@@ -60,7 +60,7 @@ let default_fb_filter_opts = {
 
 let feedback_content_tr (fb : F.feedback_content) : Serapi.Serapi_protocol.feedback_content =
   match fb with
-  | F.Message (level, loc, pp) ->
+  | F.Message (level, loc, _, pp) ->
     let str = Pp.string_of_ppcmds pp in
     Message { level; loc; pp; str }
   | F.Processed -> Processed
@@ -84,9 +84,9 @@ let feedback_tr (fb : Feedback.feedback) : Serapi.Serapi_protocol.feedback =
 
 let feedback_opt_filter ?(opts=default_fb_filter_opts) =
   let open Feedback in function
-    | { F.contents = Message (lvl, loc, msg); _ } as fb ->
+    | { F.contents = Message (lvl, loc, qf, msg); _ } as fb ->
       Some (if opts.pp_opt
-            then { fb with contents = Message(lvl, loc, coq_pp_opt msg) }
+            then { fb with contents = Message(lvl, loc, qf, coq_pp_opt msg) }
             else fb)
     | { F.contents = FileDependency _ ; _ } -> None
     | fb -> Some fb