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.
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 plugins/funind/merge.ml                 | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 40abdb68b5..507ba19701 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1405,7 +1405,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6eabe6e871..0886e7f711 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -355,8 +355,8 @@ let ind2name = Id.of_string "__ind2"
     be co-inductive, and for the moment they must not be mutual
     either. *)
 let verify_inds mib1 mib2 =
-  if not mib1.mind_finite then error "First argument is coinductive";
-  if not mib2.mind_finite then error "Second argument is coinductive";
+  if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive";
+  if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive";
   if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
   if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
   ()
@@ -885,7 +885,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,impls = Command.interp_mutual_inductive indl [] 
-          false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in
+          false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
 
-- 
cgit v1.2.3