From e20a12d92c7cc7c40ee0ac0b6569b0ee5e0e0b0f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 29 Nov 2018 15:37:26 +0100
Subject: Move shallow state logic to the function preparing state for workers

---
 proofs/proof_global.ml  | 7 ++-----
 proofs/proof_global.mli | 2 +-
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 76a1e61ad2..898fbe50f6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -462,11 +462,8 @@ module V82 = struct
 end
 
 let freeze ~marshallable =
-  match marshallable with
-  | `Yes ->
-      CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
-  | `Shallow -> !pstates
-  | `No -> !pstates
+  if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
+  else !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
 let copy_terminators ~src ~tgt =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index d9c32cf9d5..9e904c57aa 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -135,7 +135,7 @@ module V82 : sig
   Decl_kinds.goal_kind)
 end
 
-val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t
 val copy_terminators : src:t -> tgt:t -> t
-- 
cgit v1.2.3