From ecb032467557631ea60324c6afa55c91c133e40d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jun 2016 20:26:35 +0200
Subject: Reuse the typing_flags datatype for inductives.

---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 plugins/funind/merge.ml                 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f69c4d8217..c424fe1226 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1432,7 +1432,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) 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 a78eb1af76..99a165044c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,pl,impls = Command.interp_mutual_inductive true indl []
+  let mie,pl,impls = Command.interp_mutual_inductive indl []
           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 mie pl impls)
-- 
cgit v1.2.3