From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 17:33:04 +0100
Subject: Moving some universe substitution code out of the kernel.

This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
---
 tactics/ind_tables.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e1bf32f3ce..bc2fea2bd5 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -121,8 +121,7 @@ let define internal id c p univs =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
   let ctx = Evd.normalize_evar_universe_context univs in
-  let c = Vars.subst_univs_fn_constr 
-    (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
+  let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in
   let univs =
     if p then Polymorphic_const_entry (UState.context ctx)
     else Monomorphic_const_entry (UState.context_set ctx)
-- 
cgit v1.2.3