diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 15:22:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-06 14:32:23 +0200 |
| commit | 53870b7f6890a593d1da93706f3d020a79d226e5 (patch) | |
| tree | 0f6e1afa1ca58611e6a12596ef10c88359b8045e /proofs/proof.ml | |
| parent | 371566f7619aed79aad55ffed6ee0920b961be6e (diff) | |
[api] Remove (most) 8.9 deprecated objects.
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 8bbd82bb0a..70a08e4966 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -122,8 +122,6 @@ type t = { initial_euctx : UState.t } -type proof = t - (*** General proof functions ***) let proof p = @@ -435,9 +433,6 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct - let subgoals p = - let it, sigma = Proofview.proofview p.proofview in - Evd.{ it; sigma } let background_subgoals p = let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in |