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/mod_subst.mli | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'kernel/mod_subst.mli')

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 8416094063..ea391b3de7 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
   KerName.t -> KerName.t -> delta_resolver -> delta_resolver
 
 val add_inline_delta_resolver :
-  KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
+  KerName.t -> (int * constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
@@ -133,17 +133,11 @@ val subst_kn :
   substitution -> KerName.t -> KerName.t
 
 val subst_con :
-  substitution -> pconstant -> Constant.t * constr
+  substitution -> Constant.t -> Constant.t * constr Univ.univ_abstracted option
 
 val subst_pcon :
   substitution -> pconstant -> pconstant
 
-val subst_pcon_term :
-  substitution -> pconstant -> pconstant * constr
-
-val subst_con_kn :
-  substitution -> Constant.t -> Constant.t * constr
-
 val subst_constant :
   substitution -> Constant.t -> Constant.t
 
-- 
cgit v1.2.3