diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 4 |
2 files changed, 0 insertions, 5 deletions
diff --git a/library/global.ml b/library/global.ml index d9f8a6ffa3..55aed1c56e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -157,7 +157,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context let universes_of_global gr = diff --git a/library/global.mli b/library/global.mli index ca88d2dafd..76ac3f6279 100644 --- a/library/global.mli +++ b/library/global.mli @@ -131,10 +131,6 @@ val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool val is_type_in_type : GlobRef.t -> bool -val constr_of_global_in_context : Environ.env -> - GlobRef.t -> Constr.types * Univ.AUContext.t - [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"] - val type_of_global_in_context : Environ.env -> GlobRef.t -> Constr.types * Univ.AUContext.t [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"] |