Merge pull request #385 from SkySkimmer/ltac2-uncommon

Adapt to coq/coq#18528 (profile_ltac moved to engine and renamed profile_tactic)
rocq-archive · Jan 24, 2024 · 1c055b6 · 1c055b6
2 parents 85977ac + 2cf89c3
commit 1c055b6
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 8 deletions.
diff --git 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
@@ -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 → serlib/ser_profile_tactic.ml b/serlib/plugins/ltac/ser_profile_ltac.ml → 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 → serlib/ser_profile_tactic.mli b/serlib/plugins/ltac/ser_profile_ltac.mli → 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
@@ -100,14 +100,14 @@ 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 *)
 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