From 4dce356eacb7b9804c2e2398447dbbc3b0dc1383 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 29 Jun 2010 09:41:09 +0000
Subject: change the flag "internal" in declare/ind_tables from bool to a 3
 state type to allow:  * KernelVerbose / KernelSilent : handle the display of
 messages launch by Coq  * UserVerbose : handle the display of messages launch
 by user actions

Coq will still behaves the same way (TODOs in the code mark the places
where we can now change the behaviour). I'll remove them in a few days
when we'll have agreed on the correct behaviour.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/merge.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 1cf74025ab..a64ae57f56 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -906,7 +906,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
+  ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
 
 
 (* Find infos on identifier id. *)
-- 
cgit v1.2.3