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).
---
 checker/checkTypes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/checkTypes.mli')

diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
index ac9ea2fb31..9ef6ff017c 100644
--- a/checker/checkTypes.mli
+++ b/checker/checkTypes.mli
@@ -17,4 +17,4 @@ open Environ
 (*s Typing functions (not yet tagged as safe) *)
 
 val check_polymorphic_arity :
-  env -> rel_context -> template_arity -> unit
+  env -> rel_context -> template_universes -> unit
-- 
cgit v1.2.3