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

---
 checker/values.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..574019c06d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -168,8 +168,10 @@ let v_section_ctxt = v_enum "emptylist" 1
 
 (** kernel/mod_subst *)
 
+let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
+
 let v_delta_hint =
-  v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
+  v_sum "delta_hint" 0 [|[|Int; Opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
 
 let v_resolver =
   v_tuple "delta_resolver"
-- 
cgit v1.2.3