diff options
| author | Maxime Dénès | 2019-08-02 17:09:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-08-29 10:27:04 +0200 |
| commit | 2d4033152c51eb0b093c79d19a5146995af1b432 (patch) | |
| tree | b55ed207f63906531b0342b115fb1f1a321226d5 | |
| parent | 6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 (diff) | |
Fix a few wrong uses of `msg_notice`
| -rw-r--r-- | parsing/cLexer.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index de23f05a9e..7f0d768d3f 100644 --- 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 index be21a3a60d..288a349b8b 100644 --- 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 index 7362955eb7..df161b747a 100644 --- 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 index f09d202edf..b574179a93 100644 --- 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 () = |