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

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

2 files changed, 12 insertions, 3 deletions

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