diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 15:36:33 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 7a2e41abd8559d0bd4683e513dcb0b83987a9128 (patch) | |
| tree | 0a281380929879825b694d97770d07de6220a0ae | |
| parent | 49b559ccb6d17b5356bc0e43c81a8363ec0b4768 (diff) | |
[proof] Remove unused parameter in the delayed save path.
| -rw-r--r-- | tactics/proof_global.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index fe2f828fb4..7d86c6a1d1 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -226,8 +226,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in { name; entries; uctx } -let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id - (fpl : closed_proof_output Future.computation) ps = +let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.computation) ps = let { section_vars; proof; udecl; initial_euctx } = ps in let { Proof.name; poly; entry; sigma } = Proof.data proof in @@ -278,7 +277,7 @@ let return_partial_proof { proof } = proofs, Evd.evar_universe_context evd let close_future_proof ~opaque ~feedback_id ps proof = - close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps + close_proof_delayed ~opaque ~feedback_id proof ps let update_global_env = map_proof (fun p -> |