diff options
| author | Maxime Dénès | 2018-11-29 15:37:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-13 10:08:02 +0100 |
| commit | e20a12d92c7cc7c40ee0ac0b6569b0ee5e0e0b0f (patch) | |
| tree | 1c9d80fb70c9df0a28e7fc8989e931cffb787b08 /proofs | |
| parent | d9a6d4814f0669b586ca5c13d6d6540cd194b45f (diff) | |
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 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 |