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/tacmach.mli | |
| 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/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index b4cb2be2b8..3432ad4afa 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -18,9 +18,6 @@ open Locus (** Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Evd.sigma -[@@ocaml.deprecated "alias of Evd.sigma"] - open Evd type tactic = Proof_type.tactic;; @@ -29,14 +26,6 @@ val project : goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val unpackage : 'a sigma -> evar_map ref * 'a -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val repackage : evar_map ref -> 'a -> 'a sigma -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val apply_sig_tac : - evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) -[@@ocaml.deprecated "Do not use [evar_map ref]"] - val pf_concl : goal sigma -> types val pf_env : goal sigma -> env val pf_hyps : goal sigma -> named_context |