Fix a few wrong uses of msg_notice

coq · Aug 2, 2019 · b42e060 · b42e060
1 parent 264791b
commit b42e060
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
@@ -436,7 +436,7 @@ let comment_stop ep =
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
-          Feedback.msg_notice
+          Feedback.msg_debug
             (str "No begin location for comment '"
              ++ str current_s ++str"' ending at  "
              ++ int ep);

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
@@ -773,7 +773,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-             Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+             Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
@@ -1569,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
   let () = if !debug_unification then
 	     let open Pp in
-             Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++
+             Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
                                 Termops.Internal.print_constr_env env evd t1 ++ cut () ++
                                 Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
@@ -918,7 +918,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     let () = if !debug_RAKAM then
 	let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-	Feedback.msg_notice
+        Feedback.msg_debug
              (h 0 (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
 		   str "|" ++ cut () ++ Stack.pr pr stack ++
@@ -927,7 +927,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     let c0 = EConstr.kind sigma x in
     let fold () =
       let () = if !debug_RAKAM then
-	  let open Pp in Feedback.msg_notice (str "<><><><><>") in
+          let open Pp in Feedback.msg_debug (str "<><><><><>") in
       ((EConstr.of_kind c0, stack),cst_l)
     in
     match c0 with

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
@@ -30,7 +30,7 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+  Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
 let print_memory_stat () =