From 71563ebb86a83bc7cdfc17f58493f59428d764b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:49:26 +0200 Subject: Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. --- library/global.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'library/global.mli') diff --git a/library/global.mli b/library/global.mli index d6d2f1f85..0f1cec44a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -122,6 +122,13 @@ val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool +val constr_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe + context. The type 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 type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe -- cgit v1.2.3