Merge PR #12632: [state] A few nits after consolidation of state.

Reviewed-by: gares
Ack-by: SkySkimmer
Ack-by: ejgallego

3 files changed, 21 insertions, 21 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 3b7921f638..c94a6d3a5d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -834,15 +834,11 @@ module State : sig
 
   (* to send states across worker/master *)
   val get_cached : Stateid.t -> Vernacstate.t
-  val same_env : Vernacstate.t -> Vernacstate.t -> bool
-
-  type proof_part
 
   type partial_state =
     [ `Full of Vernacstate.t
-    | `ProofOnly of Stateid.t * proof_part ]
+    | `ProofOnly of Stateid.t * Vernacstate.Stm.pstate ]
 
-  val proof_part_of_frozen : Vernacstate.t -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
   (* Handlers for initial state, prior to document creation. *)
@@ -865,13 +861,9 @@ end = struct (* {{{ *)
 
   let invalidate_cur_state () = cur_id := Stateid.dummy
 
-  type proof_part = Vernacstate.Stm.pstate
-
   type partial_state =
     [ `Full of Vernacstate.t
-    | `ProofOnly of Stateid.t * proof_part ]
-
-  let proof_part_of_frozen st = Vernacstate.Stm.pstate st
+    | `ProofOnly of Stateid.t * Vernacstate.Stm.pstate ]
 
   let cache_state ~marshallable id =
     VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
@@ -924,7 +916,6 @@ end = struct (* {{{ *)
     with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
 
   let assign id what =
-    let open Vernacstate in
     if VCS.get_state id <> EmptyState then () else
     try match what with
     | `Full s ->
@@ -932,9 +923,11 @@ end = struct (* {{{ *)
            try
             let prev = (VCS.visit id).next in
             if is_cached_and_valid prev
-            then { s with lemmas =
-                PG_compat.copy_terminators
-                  ~src:((get_cached prev).lemmas) ~tgt:s.lemmas }
+            then
+              let open Vernacstate in
+              { s with
+                lemmas = PG_compat.copy_terminators
+                           ~src:((get_cached prev).lemmas) ~tgt:s.lemmas }
             else s
            with VCS.Expired -> s in
          VCS.set_state id (FullState s)
@@ -953,8 +946,6 @@ end = struct (* {{{ *)
         execution_error ?loc id (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
-  let same_env = Vernacstate.Stm.same_env
-
   (* [define] puts the system in state [id] calling [f ()] *)
   (* [safe_id] is the last known valid state before execution *)
   let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true)
@@ -1549,8 +1540,8 @@ end = struct (* {{{ *)
       match prev, this with
       | _, None -> None
       | Some (prev, o, `Cmd { cast = { expr }}), Some n
-        when is_tac expr && State.same_env o n -> (* A pure tactic *)
-          Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
+        when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *)
+          Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n))
       | Some _, Some s ->
         if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state");
           Some (id, `Full s)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index ee06205427..6d12d72408 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -267,6 +267,7 @@ module Stm = struct
           end
       }
 
+  type non_pstate = Summary.frozen * Lib.frozen
   let non_pstate { system } =
     let st = System.Stm.summary system in
     let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 16fab3782b..5efdb3cc68 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -64,15 +64,23 @@ val unfreeze_interp_state : t -> unit
 (* WARNING: Do not use, it will go away in future releases *)
 val invalidate_cache : unit -> unit
 
-(* STM-specific state handling *)
+(** STM-specific state handling *)
 module Stm : sig
+
+  (** Proof state + meta/evar counters *)
   type pstate
 
-  (** Surgery on states related to proof state *)
   val pstate : t -> pstate
   val set_pstate : t -> pstate -> t
-  val non_pstate : t -> Summary.frozen * Lib.frozen
+
+  (** Rest of the state, unfortunately this is used in low-level so we need to expose it *)
+  type non_pstate = Summary.frozen * Lib.frozen
+  val non_pstate : t -> non_pstate
+
+  (** Checks if two states have the same Environ.env (physical eq) *)
   val same_env : t -> t -> bool
+
+  (** Call [Lib.drop_objects] on the state *)
   val make_shallow : t -> t
 end