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/indTyping.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index a625caec83..babb82c39e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
   -> mutual_inductive_entry
   -> env
   * universes
+  * template_universes option
   * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
-- 
cgit v1.2.3