aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/lemmas.mli')
-rw-r--r--vernac/lemmas.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 6972edd52..1b1304db5 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
+[@@ocaml.deprecated "please use [Pfedit.get_current_context]"]