From ac2fdfb222083faa9c3893194e020bed38555ddb Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 2 Sep 2014 18:02:26 +0200
Subject: Add a [Variant] declaration which allows to write non-recursive
 variant types.

Just like the [Record] keyword allows only non-recursive records.
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 238eeb82e3..7f3417443e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -176,7 +176,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
+type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
-- 
cgit v1.2.3