diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 50a68952eb..8677b854de 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -665,4 +665,7 @@ let freeze ~marshallable = | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof +let copy_terminators ~src ~tgt = + assert(List.length src = List.length tgt); + List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 6a5116a9e7..88e047782c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -197,3 +197,4 @@ type state val freeze : marshallable:[`Yes | `No | `Shallow] -> state val unfreeze : state -> unit val proof_of_state : state -> Proof.proof +val copy_terminators : src:state -> tgt:state -> state |