Merge PR #11916: [proof] Introduce `prepare_proof` to improve normalization workflow.

Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot

2 files changed, 5 insertions, 0 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..50922ffc52 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -301,6 +301,7 @@ sig
   type t
   val repr : t -> side_effect list
   val empty : t
+  val is_empty : t -> bool
   val add : side_effect -> t -> t
   val concat : t -> t -> t
 end =
@@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
 
 let repr eff = eff.seff
 let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
 let add x es =
   if SeffSet.mem x es.elts then es
   else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +351,7 @@ let push_private_constants env eff =
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
 let concat_private = SideEffects.concat
 
 let universes_of_private eff =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f8d5d319a9..b42746a882 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 type private_constants
 
 val empty_private_constants : private_constants
+val is_empty_private_constants : private_constants -> bool
+
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)