From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 17:45:04 +0200
Subject: Add corresponding field in `VernacInductive`.

Makes sure not to generate inductive schemes of assumed positive types.
---
 intf/vernacexpr.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d7b269a1de..5fff21e270 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,7 +303,9 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * simple_binder with_coercion list
-  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of
+      bool (*[false] => assume positive*) *
+      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