From 583c6c6204052ca177bc39d90b4aa7a645a90edc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 22:06:49 +0200
Subject: [api] Reduce declare_kinds even more.

We remove two flags that were seldom used in favor of named parameters.
---
 library/decl_kinds.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 5c479255df..17746645ee 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -8,10 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Informal mathematical status of declarations *)
-
 type binding_kind = Explicit | Implicit
-
-type private_flag = bool
-
-type cumulative_inductive_flag = bool
-- 
cgit v1.2.3