diff options
| author | Maxime Dénès | 2017-11-21 13:56:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-21 13:56:15 +0100 |
| commit | 0e01de69c22a3793855b4c97c50e4514191b19bc (patch) | |
| tree | 446a0ec91c87746f946fb9352aa23fafd2b8c7f3 /proofs/proof.mli | |
| parent | 74e60947d78e3610312aa1702f12143841c5a7cf (diff) | |
| parent | 8cada511701d8893bab5553470ab721b33713043 (diff) | |
Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 48aed8225e..5756d06b64 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -65,7 +65,6 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre (*** General proof functions ***) - val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof val initial_goals : proof -> (EConstr.constr * EConstr.types) list @@ -187,6 +186,7 @@ val pr_proof : proof -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : proof -> Goal.goal list Evd.sigma |