From 1c186562c2fc628d9ec4b6cda888750a642da117 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 5 Jan 2015 16:33:20 +0100
Subject: kernel/ind Change interface of declare_mind and declare_mutual

Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
---
 plugins/funind/merge.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 8e3c0ba9c2..93b9725e50 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let mie,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 Declare.UserVerbose mie impls)
+  ignore (Command.declare_mutual_inductive_with_eliminations mie impls)
 
 
 (* Find infos on identifier id. *)
-- 
cgit v1.2.3