diff options
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 |