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 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/eConstr.ml')

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
-- 
cgit v1.2.3