From 470943bdf917caf352b5347c8d33fc39699805b0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Nov 2018 12:55:46 +0100
Subject: Fix mod_subst wrt universe polymorphism

---
 kernel/univ.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..1690bd7c70 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -963,6 +963,15 @@ struct
 
 end
 
+type 'a univ_abstracted = {
+  univ_abstracted_value : 'a;
+  univ_abstracted_binder : AUContext.t;
+}
+
+let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
+  let univ_abstracted_value = f univ_abstracted_value in
+  {univ_abstracted_value;univ_abstracted_binder}
+
 let hcons_abstract_universe_context = AUContext.hcons
 
 (** Universe info for cumulative inductive types: A context of
-- 
cgit v1.2.3