From 5bf063c15468bb81f0f48b583f600250cd829aee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:37:46 +0200
Subject: UnivGen.constr_of_glob_univ -> Constr.mkRef

---
 engine/eConstr.ml  | 6 ++++++
 engine/eConstr.mli | 2 ++
 engine/univGen.ml  | 7 +------
 engine/univGen.mli | 1 +
 4 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index cefffb315e..3385b78958 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
 
+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
+
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 
 let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e27eecc24f..1edc0ee12b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> t -> t
 
+val mkRef : GlobRef.t * EInstance.t -> t
+
 val applist : t * t list -> t
 
 val mkProd_or_LetIn : rel_declaration -> t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 64789cb808..4cdcfd9730 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -105,12 +105,7 @@ let constr_of_global gr =
               str " would forget universes.")
     else c
 
-let constr_of_global_univ (gr,u) =
-  match gr with
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConstU (sp,u)
-  | ConstructRef sp -> mkConstructU (sp,u)
-  | IndRef sp -> mkIndU (sp,u)
+let constr_of_global_univ = mkRef
 
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 4cfbb94775..82ec9f3e64 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -63,6 +63,7 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 val global_of_constr : constr -> GlobRef.t puniverses
 
 val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
 
 val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
-- 
cgit v1.2.3