From df6b72e348543a289a2ef3f89f32c905add564bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:22:59 +0200
Subject: Moving Global.type_of_global_in_context to Typeops.

It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.

Also updated the comments.
---
 kernel/typeops.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 164a47dd9a..c3a964d2db 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,6 +319,30 @@ let check_fixpoint env lna lar vdef vdeft =
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar
 
+(* Global references *)
+
+let type_of_global_in_context env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    cb.Declarations.const_type, univs
+  | IndRef ind ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+    Inductive.type_of_inductive env (specif, inst), univs
+  | ConstructRef cstr ->
+    let (mib,_ as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
+
 (************************************************************************)
 (************************************************************************)
 
-- 
cgit v1.2.3


From 09d0ba708a96125632344f2f994b45e9075fc303 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:46:15 +0200
Subject: Moving Global.constr_of_global_in_context to Typeops.

It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
---
 kernel/typeops.ml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c3a964d2db..3481d3bedb 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -343,6 +343,28 @@ 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
+
 (************************************************************************)
 (************************************************************************)
 
-- 
cgit v1.2.3