From b8a7222e670f69e024d50394afd88204e15d1b29 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 18:05:23 +0200
Subject: Less footguns in universe handling: remove subst_instance_context.

This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
---
 kernel/inductive.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be1..1eaba49aa9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx = 
-    Univ.UContext.constraints (Univ.subst_instance_context u auctx)
-  in
+  let process auctx =  Univ.AUContext.instantiate u auctx in
   match mib.mind_universes with
   | Monomorphic_ind _ -> Univ.Constraint.empty
   | Polymorphic_ind auctx -> process auctx
-- 
cgit v1.2.3