diff options
| author | Enrico Tassi | 2019-02-26 18:26:40 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-26 18:26:40 +0100 |
| commit | a6dcf744f7746942e104e26dd5341ed6d088a50a (patch) | |
| tree | 00234b542c3aa768e596965fb7a1e9b1478614d1 | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
Fix deprecation warning
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index 4e2ad92717..afb017a905 100644 --- a/library/global.mli +++ b/library/global.mli @@ -134,7 +134,7 @@ val constr_of_global_in_context : Environ.env -> val type_of_global_in_context : Environ.env -> GlobRef.t -> Constr.types * Univ.AUContext.t - [@@ocaml.deprecated "alias of [Typeops.type_of_global]"] + [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"] (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : GlobRef.t -> Univ.AUContext.t |