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.
---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 6f0ead941e..94239d0bf3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -372,7 +372,7 @@ let dummy_one_inductive_entry mie = {
 let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
   mind_entry_record = None;
-  mind_entry_finite = true;
+  mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
-- 
cgit v1.2.3