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

(limited to 'library/global.mli')

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