From 72de7e057505c45cdbf75234a9ea90465d0e19ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:15:06 +0200
Subject: Simplify fresh_foo_instance functions and pretyping of univ instance

---
 kernel/constr.ml  |  6 ++++++
 kernel/constr.mli |  3 +++
 kernel/environ.ml | 14 +++++---------
 3 files changed, 14 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index c97969c0e0..7ffde3107b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -227,6 +227,12 @@ let mkMeta  n =  Meta n
 (* Constructs a Variable named id *)
 let mkVar id = Var id
 
+let mkRef (gr,u) = let open GlobRef in match gr with
+  | ConstRef c -> mkConstU (c,u)
+  | IndRef ind -> mkIndU (ind,u)
+  | ConstructRef c -> mkConstructU (c,u)
+  | VarRef x -> mkVar x
+
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 3c9cc96a0d..12819ac39d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr
 val mkConstructU : pconstructor -> constr
 val mkConstructUi : pinductive * int -> constr
 
+(** Make a constant, inductive, constructor or variable. *)
+val mkRef : GlobRef.t Univ.puniverses -> constr
+
 (** Constructs a destructor of inductive type.
     
     [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1feb47d387..757c8773b7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -419,12 +419,6 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (subst_instance_constr u cb.const_type, csts)
 
-let constant_context env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.AUContext.empty
-  | Polymorphic_const ctx -> ctx
-
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
@@ -551,13 +545,15 @@ let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
 
 (* Universes *)
+let constant_context env c =
+  let cb = lookup_constant c env in
+  Declareops.constant_polymorphic_context cb
+
 let universes_of_global env r =
   let open GlobRef in
     match r with
     | VarRef _ -> Univ.AUContext.empty
-    | ConstRef c ->
-      let cb = lookup_constant c env in
-      Declareops.constant_polymorphic_context cb
+    | ConstRef c -> constant_context env c
     | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
       let mib = lookup_mind mind env in
       Declareops.inductive_polymorphic_context mib
-- 
cgit v1.2.3