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/environ.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..7835a807ba 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -241,6 +241,8 @@ let is_impredicative_set env =
 let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
+let indices_matter env = env.env_typing_flags.indices_matter
+
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context.env_named_ctx
 let named_context_val env = env.env_named_context
@@ -389,6 +391,7 @@ let same_flags {
      check_guarded;
      check_universes;
      conv_oracle;
+     indices_matter;
      share_reduction;
      enable_VM;
      enable_native_compiler;
@@ -396,6 +399,7 @@ let same_flags {
   check_guarded == alt.check_guarded &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
+  indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
   enable_native_compiler == alt.enable_native_compiler
-- 
cgit v1.2.3