diff options
| author | Emilio Jesus Gallego Arias | 2019-03-01 12:27:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-01 12:27:12 +0100 |
| commit | ed5685a2afaa9c429d1f16950317363d9b0bc1a8 (patch) | |
| tree | 9505cc48305c96a668cb3daf9613bc4600e4334b | |
| parent | ebdcaa393b1f332ad917b33bf9d7a222d3faa7c4 (diff) | |
| parent | a6dcf744f7746942e104e26dd5341ed6d088a50a (diff) | |
Merge PR #9656: Fix deprecation warning
Reviewed-by: ejgallego
| -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 |