diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 02:45:47 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:16:22 -0400 |
| commit | e9c05828bba7ceb696a5c17457b8e0826bbd94f1 (patch) | |
| tree | fa9f93732095d304aff28239b7293ae6c1bbb075 /stm | |
| parent | b755869a7fdb34dcf7dacc9d5fd93c768d71d751 (diff) | |
[proof] Split return_proof in partial and regular versions.
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ba8eba0eed..c1156b9afe 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1501,7 +1501,7 @@ end = struct (* {{{ *) let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - let p = PG_compat.return_proof ~allow_partial:drop_pt () in + let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in if drop_pt then feedback ~id Complete; p) @@ -1661,7 +1661,7 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then - let _proof = PG_compat.return_proof ~allow_partial:true () in + let _proof = PG_compat.return_partial_proof () in `OK_ADMITTED else begin let opaque = Proof_global.Opaque in |