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

---
 engine/eConstr.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..e27eecc24f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -180,6 +180,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 (** Pops lambda abstractions until there are no more, skipping casts. *)
-- 
cgit v1.2.3


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

(limited to 'engine/eConstr.mli')

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