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

2 files changed, 15 insertions, 8 deletions

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. *)
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 676863b782..336ae2ccde 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -408,7 +408,11 @@ let kind_of_global_goal = function
 let kind_of_inductive isrecord kn =
  "DEFINITION",
  if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
- then if isrecord then "Record" else "Inductive"
+ then begin 
+   match isrecord with 
+   | Declare.KernelSilent -> "Record"
+   | _ -> "Inductive"
+ end
  else "CoInductive"
 ;;
 
@@ -478,8 +482,8 @@ let kind_of_global r =
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
       let isrecord =
-	try let _ = Recordops.lookup_projections kn in true
-        with Not_found -> false in
+	try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
+        with Not_found -> Declare.KernelVerbose in
       kind_of_inductive isrecord (fst kn)
   | Ln.VarRef id -> kind_of_variable id
   | Ln.ConstRef kn -> kind_of_constant kn
@@ -539,13 +543,15 @@ let print internal glob_ref kind xml_library_root =
   in
   let fn = filename_of_path xml_library_root tag in
   let uri = Cic2acic.uri_of_kernel_name tag in
-   if not internal then print_object_kind uri kind;
+  (match internal with
+    | Declare.KernelSilent -> ()
+    | _ -> print_object_kind uri kind);
    print_object uri obj Evd.empty None fn
 ;;
 
 let print_ref qid fn =
   let ref = Nametab.global qid in
-  print false ref (kind_of_global ref) fn
+  print Declare.UserVerbose ref (kind_of_global ref) fn
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
@@ -580,7 +586,7 @@ let _ =
   Declare.set_xml_declare_variable
    (function (sp,kn) ->
      let id = Libnames.basename sp in
-     print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+     print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
      proof_to_export := None)
 ;;
 
@@ -603,7 +609,8 @@ let _ =
 let _ =
   Declare.set_xml_declare_inductive
    (function (isrecord,(sp,kn)) ->
-      print false (Libnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn))
+      print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0))
+        (kind_of_inductive isrecord (Names.mind_of_kn kn))
         xml_library_root)
 ;;