diff options
| author | Pierre-Marie Pédrot | 2019-04-30 12:01:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-30 12:01:33 +0200 |
| commit | 823bde2eaffbacdb7a3a08c9d7274cd84dc5bef5 (patch) | |
| tree | 5dcdd721941d9b88ec90eec3503fb65306806823 /library | |
| parent | 7d5b28d91df46db3f5e4b02093b64a18d67a1aa2 (diff) | |
| parent | 478db417e1a3a493870f012495bbc7348581ac17 (diff) | |
Merge PR #9952: Remove `constr_of_global_in_context`
Reviewed-by: ppedrot
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]"] |