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

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 16ca444e3a..34ed33f949 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -599,7 +599,7 @@ let rec lambda_of_constr env sigma c =
 	    { asw_ind = ind;
           asw_ci = ci;
           asw_reloc = tbl; 
-          asw_finite = mib.mind_finite;
+          asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
           asw_prefix = prefix}
       in
       (* translation of the argument *)
-- 
cgit v1.2.3