From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 intf/decl_kinds.ml | 4 +++-
 intf/vernacexpr.ml | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 8254b1b802..c15c009887 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
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index cabd06735f..26a6db4ec9 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -336,7 +336,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-- 
cgit v1.2.3