From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 17:45:04 +0200
Subject: Add corresponding field in `VernacInductive`.

Makes sure not to generate inductive schemes of assumed positive types.
---
 plugins/funind/merge.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/merge.ml')

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580b9..8c4bd484f5 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -884,7 +884,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,impls = Command.interp_mutual_inductive indl [] 
+  let mie,impls = Command.interp_mutual_inductive true 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 impls)
-- 
cgit v1.2.3