From b18b40878f071b6c7d67d1a2d031370f7a498d0b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 11:40:27 +0200
Subject: Print [Variant] types with the keyword [Variant].

Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
---
 kernel/declarations.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2c516cafd6..6b3f6c72f4 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -158,7 +158,7 @@ type mutual_inductive_body = {
 	In the case it is primitive we get its projection names and checked
 	projection bodies, otherwise both arrays are empty. *)
 
-    mind_finite : bool;  (** Whether the type is inductive or coinductive *)
+    mind_finite : Decl_kinds.recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-- 
cgit v1.2.3