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

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..d1d184df69 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -24,6 +24,7 @@ let safe_flags oracle = {
   share_reduction = true;
   enable_VM = true;
   enable_native_compiler = true;
+  indices_matter = true;
 }
 
 (** {6 Arities } *)
-- 
cgit v1.2.3