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

---
 library/global.ml  | 1 +
 library/global.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 4ea5969a6f..67b00cf411 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -88,6 +88,7 @@ let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
diff --git a/library/global.mli b/library/global.mli
index 01ee695c49..40962e21af 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,6 +29,7 @@ val named_context : unit -> Constr.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val typing_flags : unit -> Declarations.typing_flags
 
-- 
cgit v1.2.3