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/vars.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index f9c576ca4a..bd56d60053 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,6 +295,11 @@ let subst_instance_constr subst c =
     in
     aux c
 
+let univ_instantiate_constr u c =
+  let open Univ in
+  assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
+  subst_instance_constr u c.univ_abstracted_value
+
 (* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
 (* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
 
-- 
cgit v1.2.3