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

---
 pretyping/classops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f18040accb..306a76e35e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,9 +192,11 @@ let subst_cl_typ subst ct = match ct with
     let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
-      let c',t = subst_con_kn subst c in
-	if c' == c then ct else
-         pi1 (find_class_type Evd.empty (EConstr.of_constr t))
+      let c',t = subst_con subst c in
+      if c' == c then ct else (match t with
+          | None -> CL_CONST c'
+          | Some t ->
+            pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
   | CL_IND i ->
       let i' = subst_ind subst i in
 	if i' == i then ct else CL_IND i'
-- 
cgit v1.2.3