2 files changed, 20 insertions, 7 deletions
diff --git a/library/declare.ml b/library/declare.ml
index b571ecf3a4..2886c63d85 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -25,11 +25,17 @@ open Cooking
 open Decls
 open Decl_kinds
 
+(** flag for internal message display *)
+type internal_flag = 
+  | KernelVerbose (* kernel action, a message is displayed *)
+  | KernelSilent  (* kernel action, no message is displayed *)
+  | UserVerbose   (* user action, a message is displayed *)
+
 (** XML output hooks *)
 
 let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
+let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
 
 let if_xml f x = if !Flags.xml_export then f x else ()
 
@@ -172,8 +178,10 @@ let declare_constant_gen internal id (cd,kind) =
   !xml_declare_constant (internal,kn);
   kn
 
-let declare_internal_constant = declare_constant_gen true
-let declare_constant = declare_constant_gen false
+(* TODO: add a third function to distinguish between KernelVerbose
+ * and user Verbose *)
+let declare_internal_constant = declare_constant_gen KernelSilent
+let declare_constant = declare_constant_gen UserVerbose
 
 (** Declaration of inductive blocks *)
 
diff --git a/library/declare.mli b/library/declare.mli
index 3ff91cc5e7..3847a4ab94 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -44,6 +44,11 @@ type constant_declaration = constant_entry * logical_kind
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration *)
+type internal_flag =
+  | KernelVerbose
+  | KernelSilent
+  | UserVerbose
+
 val declare_constant :
  identifier -> constant_declaration -> constant
 
@@ -53,12 +58,12 @@ val declare_internal_constant :
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
-val declare_mind : bool -> mutual_inductive_entry -> object_name
+val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
 (** Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * constant -> unit) -> unit
-val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
+val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
 
 (** Hook for the cache function of constants and inductives *)
 val add_cache_hook : (full_path -> unit) -> unit