From 8cada511701d8893bab5553470ab721b33713043 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 02:55:51 +0100 Subject: [proof] Attempt to deprecate some V82 parts of the proof API. I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. --- proofs/proof.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/proof.mli') diff --git a/proofs/proof.mli b/proofs/proof.mli index 48aed8225..5756d06b6 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 -- cgit v1.2.3