diff options
| author | Enrico Tassi | 2018-12-17 10:30:59 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-17 10:30:59 +0100 |
| commit | 40ca052fc89df366bf8de884dcc7a11d1b613e9f (patch) | |
| tree | bea66d05842350191a51361e5e97b8863ed63494 /proofs | |
| parent | 7e155688331c8f004f34950da67108d7284e4e56 (diff) | |
| parent | 6e34168a3513ace5beda5b8bd32ea85aecf0b15a (diff) | |
Merge PR #9220: Move shallow state logic to the function preparing state for workers
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
2 files changed, 3 insertions, 6 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2027ad4e21..8077da8807 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 |