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

(limited to 'kernel/constr.ml')

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


From 5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:27:27 +0200
Subject: Simplify vars_of_global usage

---
 kernel/constr.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 7ffde3107b..b490aa5092 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -407,6 +407,12 @@ let destCoFix c = match kind c with
   | CoFix cofix -> cofix
   | _ -> raise DestKO
 
+let destRef c = let open GlobRef in match kind c with
+  | Var x -> VarRef x, Univ.Instance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
 
 (******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
-- 
cgit v1.2.3