v13392 port from v8.3 to trunk : correct message when defining inductive schemes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13394 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 13 insertions, 22 deletions

diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 7ddf2b3fc..974b74a6d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -159,7 +159,6 @@ 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 ->
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index d7a2b03df..3b090e79e 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -170,17 +170,15 @@ let beq_scheme_msg mind =
 let declare_beq_scheme_with 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 KernelSilent [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] 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
@@ -190,7 +188,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 KernelSilent None ind)
+    ignore (define_individual_scheme dep KernelVerbose None ind)
 
 (* Induction/recursion schemes *)
 
@@ -204,7 +202,6 @@ 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
@@ -214,7 +211,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 KernelSilent None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -239,48 +236,44 @@ let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
     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 KernelSilent [] kn
+    declare_eq_decidability_gen KernelVerbose [] 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 KernelSilent None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind);
     ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      KernelSilent None ind);
+      KernelVerbose 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 KernelSilent None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose 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 KernelSilent None ind)
+      ignore (define_individual_scheme congr_scheme_kind KernelVerbose 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 KernelSilent None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind
 
 (* Scheme command *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c6f3dd0d7..0b338fdd8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -257,8 +257,7 @@ 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
-(* TODO : maybe switch to KernelVerbose *)
-  let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose 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