diff options
| author | Maxime Dénès | 2019-04-12 15:23:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-12 15:25:09 +0200 |
| commit | 478db417e1a3a493870f012495bbc7348581ac17 (patch) | |
| tree | e7355bd68247bc16f02d0c077ab914bc041c257d /library | |
| parent | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (diff) | |
Remove `constr_of_global_in_context`
This function seems unused.
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]"] |