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

(limited to 'kernel/constr.mli')

diff --git a/kernel/constr.mli b/kernel/constr.mli
index 12819ac39d..c012f04260 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -343,6 +343,8 @@ val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
 
+val destRef : constr -> GlobRef.t Univ.puniverses
+
 (** {6 Equality} *)
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
-- 
cgit v1.2.3