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/indtypes.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a827c17683..840e23ed69 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -50,8 +50,3 @@ val check_positivity : chkpos:bool ->
 (** The following function does checks on inductive declarations. *)
 
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** The following enforces a system compatible with the univalent model *)
-
-val enforce_indices_matter : unit -> unit
-val is_indices_matter : unit -> bool
-- 
cgit v1.2.3