aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/decl_kinds.ml
diff options
context:
space:
mode:
Diffstat (limited to 'intf/decl_kinds.ml')
-rw-r--r--intf/decl_kinds.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 8254b1b80..c15c00988 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -14,7 +14,9 @@ type binding_kind = Explicit | Implicit
type polymorphic = bool
-type private_flag = bool
+type private_flag = bool
+
+type cumulative_inductive_flag = bool
type theorem_kind =
| Theorem