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.ml  | 19 +++++++++++++++++++
 library/global.mli |  7 +++++++
 2 files changed, 26 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 3a74f535d9..5fff265663 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -191,6 +191,25 @@ let type_of_global_unsafe r =
     let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
     Inductive.type_of_constructor (cstr,inst) specif
 
+let constr_of_global_in_context env r =
+  let open Constr in
+  match r with
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.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, oib as specif) = 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,oib as specif) =
+      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
+
 let type_of_global_in_context env r = 
   match r with
   | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
diff --git a/library/global.mli b/library/global.mli
index d6d2f1f851..0f1cec44a5 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