From 2cf89c3e3cfd9a4f86abfbff36ce095f70b0a5fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 23 Jan 2024 13:38:47 +0100
Subject: [PATCH] Adapt to coq/coq#18528 (profile_ltac moved to engine and
 renamed profile_tactic)

---
 serapi/serapi_protocol.ml                                     | 4 ++--
 serapi/serapi_protocol.mli                                    | 2 +-
 .../ltac/ser_profile_ltac.ml => ser_profile_tactic.ml}        | 2 +-
 .../ltac/ser_profile_ltac.mli => ser_profile_tactic.mli}      | 4 +---
 sertop/sertop_ser.ml                                          | 2 +-
 5 files changed, 6 insertions(+), 8 deletions(-)
 rename serlib/{plugins/ltac/ser_profile_ltac.ml => ser_profile_tactic.ml} (97%)
 rename serlib/{plugins/ltac/ser_profile_ltac.mli => ser_profile_tactic.mli} (95%)

diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
index c75671d0..a0c8d8e3 100644
--- a/serapi/serapi_protocol.ml
+++ b/serapi/serapi_protocol.ml
@@ -130,7 +130,7 @@ type coq_object =
   | CoqGlobRef   of Names.GlobRef.t
   | CoqGlobRefExt of Globnames.extended_global_reference
   | CoqImplicit  of Impargs.implicits_list
-  | CoqProfData  of Profile_ltac.treenode
+  | CoqProfData  of Profile_tactic.treenode
   | CoqNotation  of Constrexpr.notation
   | CoqUnparsing of Ppextend.notation_printing_rules * Notation_gram.notation_grammar
   | CoqGoal      of Constr.t               Serapi_goals.reified_goal Serapi_goals.ser_goals
@@ -600,7 +600,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
   | Tactics prefix -> List.map (fun (i,t) -> CoqTactic(i,t)) @@ QueryUtil.query_tactics prefix
   | Locate  id     -> List.map (fun qid -> CoqQualId qid) @@ QueryUtil.locate id
   | Implicits id   -> List.map (fun ii -> CoqImplicit ii ) @@ QueryUtil.implicits id
-  | ProfileData    -> [CoqProfData (Profile_ltac.get_local_profiling_results ())]
+  | ProfileData    -> [CoqProfData (Profile_tactic.get_local_profiling_results ())]
   | Proof          -> QueryUtil.get_proof ~pstate
   | Unparsing ntn  -> (* Unfortunately this will produce an anomaly if the notation is not found...
                        * To keep protocol promises we need to special wrap it.
diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli
index 036e93d4..ebc9aa29 100644
--- a/serapi/serapi_protocol.mli
+++ b/serapi/serapi_protocol.mli
@@ -215,7 +215,7 @@ type coq_object =
   (** "Extended Global Reference", as they can contain syntactic definitions too *)
   | CoqImplicit  of Impargs.implicits_list
   (** Implicit status for a constant *)
-  | CoqProfData  of Profile_ltac.treenode
+  | CoqProfData  of Profile_tactic.treenode
   (** Ltac Profiler data *)
   | CoqNotation  of Constrexpr.notation
   (** Representation of a notation (usually a string) *)
diff --git a/serlib/plugins/ltac/ser_profile_ltac.ml b/serlib/ser_profile_tactic.ml
similarity index 97%
rename from serlib/plugins/ltac/ser_profile_ltac.ml
rename to serlib/ser_profile_tactic.ml
index cb325573..c2e75ee6 100644
--- a/serlib/plugins/ltac/ser_profile_ltac.ml
+++ b/serlib/ser_profile_tactic.ml
@@ -33,7 +33,7 @@ let sexp_of_cstring_map f m =
   sexp_of_list s_f l
 
 type treenode =
-  [%import: Ltac_plugin.Profile_ltac.treenode
+  [%import: Profile_tactic.treenode
   [@with CString.Map.t   := cstring_map;
          CString.Map.key := string
   ]]
diff --git a/serlib/plugins/ltac/ser_profile_ltac.mli b/serlib/ser_profile_tactic.mli
similarity index 95%
rename from serlib/plugins/ltac/ser_profile_ltac.mli
rename to serlib/ser_profile_tactic.mli
index 2dc8b7eb..4966b41e 100644
--- a/serlib/plugins/ltac/ser_profile_ltac.mli
+++ b/serlib/ser_profile_tactic.mli
@@ -15,9 +15,7 @@
 
 open Sexplib
 
-open Ltac_plugin
-
-type treenode = Profile_ltac.treenode
+type treenode = Profile_tactic.treenode
 
 val treenode_of_sexp : Sexp.t -> treenode
 val sexp_of_treenode : treenode -> Sexp.t
diff --git a/sertop/sertop_ser.ml b/sertop/sertop_ser.ml
index 8d3ce762..fb73d540 100644
--- a/sertop/sertop_ser.ml
+++ b/sertop/sertop_ser.ml
@@ -100,6 +100,7 @@ module Notation_gram = Ser_notation_gram
 module Genarg     = Ser_genarg
 module Loadpath   = Ser_loadpath
 module Printer    = Ser_printer
+module Profile_tactic = Ser_profile_tactic
 
 (* Alias fails due to the [@@default in protocol] *)
 (* module Stm        = Ser_stm *)
@@ -107,7 +108,6 @@ module Ser_stm    = Ser_stm
 
 module Ltac_plugin = struct
   module Tacenv       = Serlib_ltac.Ser_tacenv
-  module Profile_ltac = Serlib_ltac.Ser_profile_ltac
   module Tacexpr      = Serlib_ltac.Ser_tacexpr
 end