aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r--pretyping/reductionops.ml4
1 files changed, 2 insertions, 2 deletions
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