From 60d2e06769abee8e7ebc9b9cc9febf05c8f8994a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Jul 2020 18:56:01 +0200
Subject: [state] A few nits after consolidation of state.

We remove some dead aliases and add some documentation to the
interface file.
---
 vernac/vernacstate.ml  |  1 +
 vernac/vernacstate.mli | 14 +++++++++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'vernac')

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
 
-- 
cgit v1.2.3