aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.mli')
-rw-r--r--proofs/tacmach.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de96f8510..31496fb3d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ 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