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/declarations.ml | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156..94832726fe 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -61,13 +61,27 @@ type constant_universes =
     of a constant are tracked in their {!constant_body} so that they
     can be displayed to the user. *)
 type typing_flags = {
-  check_guarded : bool; (** If [false] then fixed points and co-fixed
-                            points are assumed to be total. *)
-  check_universes : bool; (** If [false] universe constraints are not checked *)
-  conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
-  share_reduction : bool; (** Use by-need reduction algorithm *)
-  enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
-  enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
+  check_guarded : bool;
+  (** If [false] then fixed points and co-fixed points are assumed to
+      be total. *)
+
+  check_universes : bool;
+  (** If [false] universe constraints are not checked *)
+
+  conv_oracle : Conv_oracle.oracle;
+  (** Unfolding strategies for conversion *)
+
+  share_reduction : bool;
+  (** Use by-need reduction algorithm *)
+
+  enable_VM : bool;
+  (** If [false], all VM conversions fall back to interpreted ones *)
+
+  enable_native_compiler : bool;
+  (** If [false], all native conversions fall back to VM ones *)
+
+  indices_matter: bool;
+  (** The universe of an inductive type must be above that of its indices. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
-- 
cgit v1.2.3