From e0bcbccf437ebee4157fdfdd5cba7b42019ead27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Mar 2020 10:57:19 +0100
Subject: Ensure that template parameters are shared in the same inductive
 block.

This could have been at the root of strange behaviours (read unsoundness).
---
 kernel/inductive.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b690fe1157..90571844b9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : Sorts.t array -> Universe.t
 
-val instantiate_universes : Constr.rel_context ->
-  template_arity -> param_univs -> Constr.rel_context * Sorts.t
-
 (** {6 Debug} *)
 
 type size = Large | Strict
-- 
cgit v1.2.3