From ec209ea02cb8fa86f09aff88d0464c865ed7b8a5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 13 Nov 2018 16:02:03 +0100
Subject: Put -indices-matter in typing_flags

---
 kernel/indtypes.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20c90bc05a..a4a02791b4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -35,14 +35,6 @@ env_ar_par = env_ar + declaration of parameters
 nmr = ongoing computation of recursive parameters
 *)
 
-(* Tell if indices (aka real arguments) contribute to size of inductive type *)
-(* If yes, this is compatible with the univalent model *)
-
-let indices_matter = ref false
-
-let enforce_indices_matter () = indices_matter := true
-let is_indices_matter () = !indices_matter
-
 (* [weaker_noccur_between env n nvars t] (defined above), checks that
    no de Bruijn indices between [n] and [n+nvars] occur in [t]. If
    some such occurrences are found, then reduction is performed
@@ -303,7 +295,7 @@ let typecheck_inductive env mie =
 	 let inflev = 
 	   (* The level of the inductive includes levels of indices if 
 	      in indices_matter mode *)
-	     if !indices_matter 
+             if indices_matter env
 	     then Some (cumulate_arity_large_levels env_params sign)
 	     else None
 	 in
-- 
cgit v1.2.3