diff options
| author | Emilio Jesus Gallego Arias | 2019-09-04 15:00:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-04 15:00:03 +0200 |
| commit | 6a6a2575c10d05cd0151a83c133825d43bd3cb28 (patch) | |
| tree | a46211ebfa7af615d7edd8359208f8e5dcd5af1d /pretyping | |
| parent | bcf2dae1e39c6ff27c574a82c4451323a673b15f (diff) | |
| parent | 2d4033152c51eb0b093c79d19a5146995af1b432 (diff) | |
Merge PR #10612: Fix feedback levels
Ack-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
2 files changed, 4 insertions, 4 deletions
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 |