diff options
| -rw-r--r-- | kernel/typeops.ml | 22 | ||||
| -rw-r--r-- | kernel/typeops.mli | 8 | ||||
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 4 |
4 files changed, 0 insertions, 35 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 12ffbf4357..af710e7822 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -462,28 +462,6 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs -(* Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -let constr_of_global_in_context env r = - let open GlobRef in - match r with - | VarRef id -> mkVar id, Univ.AUContext.empty - | ConstRef c -> - let cb = lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - mkConstU (c, Univ.make_abstract_instance univs), univs - | IndRef ind -> - let (mib,_) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - mkIndU (ind, Univ.make_abstract_instance univs), univs - | ConstructRef cstr -> - let (mib,_) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - mkConstructU (cstr, Univ.make_abstract_instance univs), univs - (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index cc1885f42d..c8f3e506e6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -107,14 +107,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t usage. For non-universe-polymorphic constants, it does not matter. *) -(** {6 Building a term from a global reference *) - -(** Map a global reference to a term in its local universe - context. The term should not be used without pushing it's universe - context in the environmnent of usage. For non-universe-polymorphic - constants, it does not matter. *) -val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t - (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) 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]"] |