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

6 files changed, 50 insertions, 30 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4259ccb81c..21fb277e2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -363,7 +363,7 @@ let do_mutual_inductive indl finite =
   (* Interpret the types *)
   let mie,impls = interp_mutual_inductive indl ntns finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (declare_mutual_inductive_with_eliminations false mie impls);
+  ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b056afa58d..779e77f313 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -82,7 +82,7 @@ val interp_mutual_inductive :
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
-  bool -> mutual_inductive_entry -> one_inductive_impls list ->
+  Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list ->
   mutual_inductive
 
 (** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 8e3d9437f8..4e8d861000 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -110,7 +110,11 @@ let declare_scheme kind indcl =
   Lib.add_anonymous_leaf (inScheme (kind,indcl))
 
 let define internal id c =
-  let fd = if internal then declare_internal_constant else declare_constant in
+  (* TODO: specify even more by distinguish between KernelVerbose and
+   * UserVerbose *)
+  let fd = match internal with 
+    | KernelSilent -> declare_internal_constant
+    | _ -> declare_constant in
   let kn = fd id
     (DefinitionEntry
       { const_entry_body = c;
@@ -118,7 +122,9 @@ let define internal id c =
         const_entry_opaque = false;
 	const_entry_boxed = Flags.boxed_definitions() },
       Decl_kinds.IsDefinition Scheme) in
-  if not internal then definition_message id;
+  (match internal with
+  | KernelSilent -> ()
+  | _-> definition_message id);
   kn
 
 let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
@@ -153,14 +159,15 @@ let define_mutual_scheme kind internal names mind =
   | s,MutualSchemeFunction f ->
       define_mutual_scheme_base kind s f internal names mind
 
+(* TODO: change KernelSilent here to the right behaviour *)
 let find_scheme kind (mind,i as ind) =
   try Stringmap.find kind (Indmap.find ind !scheme_map)
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f true None ind
+      define_individual_scheme_base kind s f KernelSilent None ind
   | s,MutualSchemeFunction f ->
-      (define_mutual_scheme_base kind s f true [] mind).(i)
+      (define_mutual_scheme_base kind s f KernelSilent [] mind).(i)
 
 let check_scheme kind ind =
   try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 0d3a250c95..babc2d9209 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -39,10 +39,11 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
 
 (** Force generation of a (mutually) scheme with possibly user-level names *)
 
-val define_individual_scheme : individual scheme_kind -> bool (** internal *) ->
+val define_individual_scheme : individual scheme_kind -> 
+  Declare.internal_flag (** internal *) ->
   identifier option -> inductive -> constant
 
-val define_mutual_scheme : mutual scheme_kind -> bool (** internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
   (int * identifier) list -> mutual_inductive -> constant array
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a02b01351f..03813c9d48 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -100,7 +100,10 @@ let _ =
 (* Util *)
 
 let define id internal c t =
-  let f = if internal then declare_internal_constant else declare_constant in
+  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+  let f = match internal with
+   | KernelSilent -> declare_internal_constant
+   | _ -> declare_constant in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
@@ -118,12 +121,13 @@ let declare_beq_scheme_gen internal names kn =
 
 let alarm what internal msg =
   let debug = false in
-  if internal then
+  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+  match internal with
+  | KernelSilent ->
     (if debug then
       Flags.if_verbose Pp.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
-  else
-    errorlabstrm "" msg
+  | _ -> errorlabstrm "" msg
 
 let try_declare_scheme what f internal names kn =
   try f internal names kn
@@ -164,18 +168,19 @@ let beq_scheme_msg mind =
     (list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
 
 let declare_beq_scheme_with l kn =
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen false l kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
 
+(* TODO : maybe switch to KernelVerbose to have the right behaviour *)
 let try_declare_beq_scheme kn =
   (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen true [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
 (* Case analysis schemes *)
-
+(* TODO: maybe switch to KernelVerbose *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -185,7 +190,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        apropriate type *)
   if List.mem InType kelim then
-    ignore (define_individual_scheme dep true None ind)
+    ignore (define_individual_scheme dep KernelSilent None ind)
 
 (* Induction/recursion schemes *)
 
@@ -199,6 +204,7 @@ let kinds_from_type =
    InProp,ind_dep_scheme_kind_from_type;
    InSet,rec_dep_scheme_kind_from_type]
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -208,7 +214,7 @@ let declare_one_induction_scheme ind =
     list_map_filter (fun (sort,kind) ->
       if List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
-  List.iter (fun kind -> ignore (define_individual_scheme kind true None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -231,45 +237,50 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
 
 let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen false l kn
+    declare_eq_decidability_gen UserVerbose l kn
 
+(* TODO:  maybe switch to kernel verbose *)
 let try_declare_eq_decidability kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen true [] kn
+    declare_eq_decidability_gen KernelSilent [] kn
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
 let ignore_error f x = try ignore (f x) with _ -> ()
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind true None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind true None ind);
-    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
+      KernelSilent None ind);
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
-    ignore_error (define_individual_scheme rew_l2r_scheme_kind true None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind true None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
   end
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with _ -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind true None ind)
+      ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind)
     else
       warning "Cannot build congruence scheme because eq is not found"
   end
 
+(* TODO: maybe switch to kernel verbose *)
 let declare_sym_scheme ind =
   if Hipattern.is_inductive_equality ind then
     (* Expect the equality to be symmetric *)
-    ignore_error (define_individual_scheme sym_scheme_kind true None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind
 
 (* Scheme command *)
 
@@ -337,7 +348,7 @@ let do_mutual_induction_scheme lnamedepindsort =
   let rec declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 Evd.empty decl in
     let decltype = refresh_universes decltype in
-    let cst = define fi false decl (Some decltype) in
+    let cst = define fi UserVerbose decl (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -432,7 +443,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  ignore (define (snd name) false body (Some typ));
+  ignore (define (snd name) UserVerbose body (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e4177b0fc1..89bf769114 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -259,7 +259,8 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_record = true;
       mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
-  let kn = Command.declare_mutual_inductive_with_eliminations true mie [(paramimpls,[])] in
+(* TODO : maybe switch to KernelVerbose *)
+  let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in