Imported Upstream version 8.3upstream/8.3

1 files changed, 14 insertions, 20 deletions

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 29d7a12c..9031d8a3 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *)
+(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *)
 
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
@@ -123,8 +123,8 @@ let declare_beq_scheme_gen internal names kn =
 
 let alarm what internal msg =
   let debug = false in
-  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
   match internal with
+  | KernelVerbose 
   | KernelSilent ->
     (if debug then
       Flags.if_verbose Pp.msg_warning
@@ -172,17 +172,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
@@ -192,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 KernelSilent None ind)
+    ignore (define_individual_scheme dep KernelVerbose None ind)
 
 (* Induction/recursion schemes *)
 
@@ -206,7 +204,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
@@ -216,7 +213,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 =
@@ -241,10 +238,9 @@ 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 []
 
@@ -252,36 +248,34 @@ let ignore_error f x = try ignore (f x) with _ -> ()
 
 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 *)