aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/system.ml4
-rw-r--r--library/goptions.ml4
-rw-r--r--plugins/cc/cctac.ml43
-rw-r--r--plugins/extraction/g_extraction.mlg4
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg6
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ssr/ssrvernac.mlg8
-rw-r--r--tactics/auto.ml16
-rw-r--r--tactics/eauto.ml8
-rw-r--r--test-suite/output/auto.out16
-rw-r--r--vernac/vernacentries.ml2
13 files changed, 57 insertions, 62 deletions
diff --git a/lib/system.ml b/lib/system.ml
index b1a9efccfc..8c333ec267 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -300,13 +300,13 @@ let with_time ~batch ~header f x =
let y = f x in
let tend = get_time() in
let msg2 = if batch then "" else " (successful)" in
- Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
y
with e ->
let tend = get_time() in
let msg = if batch then "" else "Finished failing transaction in " in
let msg2 = if batch then "" else " (failure)" in
- Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
(* We use argv.[0] as we don't want to resolve symlinks *)
diff --git a/library/goptions.ml b/library/goptions.ml
index c7024ca81d..0973944fb5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -398,9 +398,9 @@ let print_option_value key =
let s = read () in
match s with
| BoolValue b ->
- Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
| _ ->
- Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
let get_tables () =
let tables = !value_tab in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3ed843649e..b5be1cdd89 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms =
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
discriminate_tac cstr p
| Incomplete ->
- let open Glob_term in
- let env = Proofview.Goal.env gl in
- let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
- let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
- let pr_missing (c, missing) =
- let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
- let holes = List.init missing (fun _ -> hole) in
- Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
- in
- Feedback.msg_info
- (Pp.str "Goal is solvable by congruence but some arguments are missing.");
- Feedback.msg_info
- (Pp.str " Try " ++
- hov 8
- begin
- str "\"congruence with (" ++
- prlist_with_sep
- (fun () -> str ")" ++ spc () ++ str "(")
- pr_missing
- terms_to_complete ++
- str ")\","
- end ++
- Pp.str " replacing metavariables by arbitrary terms.");
- Tacticals.New.tclFAIL 0 (str "Incomplete")
+ let open Glob_term in
+ let env = Proofview.Goal.env gl in
+ let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+ let pr_missing (c, missing) =
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+ let holes = List.init missing (fun _ -> hole) in
+ Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+ in
+ let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+ ++ fnl () ++
+ str " Try " ++
+ hov 8
+ begin
+ str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
+ pr_missing terms_to_complete ++ str ")\","
+ end ++
+ str " replacing metavariables by arbitrary terms.") in
+ Tacticals.New.tclFAIL 0 msg
| Contradiction dis ->
let env = Proofview.Goal.env gl in
let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index e222fbc808..4f077b08b6 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -128,7 +128,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> {Feedback. msg_info (print_extraction_inline ()) }
+ -> {Feedback.msg_notice (print_extraction_inline ()) }
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -150,7 +150,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> { Feedback.msg_info (print_extraction_blacklist ()) }
+ -> { Feedback.msg_notice (print_extraction_blacklist ()) }
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8a5c32b8b5..35cd10a1ff 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -83,7 +83,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> {
- Feedback.msg_info
+ Feedback.msg_notice
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 21d61d1f97..f7215a9d13 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 455c8ab003..61cc77c42a 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -145,7 +145,7 @@ open Pp
VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> {
- Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
+ Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END
VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
END
{
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
let finish_timing ~prefix name =
let tend = System.get_time () in
let tstart = get_timer name in
- Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+ Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
System.fmt_time_difference tstart tend)
(* ******************** *)
@@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter =
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results Local.(CList.last !stack) in
- Feedback.msg_info (to_string ~cutoff ~filter results)
+ Feedback.msg_notice (to_string ~cutoff ~filter results)
;;
let print_results ~cutoff =
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index f3f1d713e9..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -279,7 +279,7 @@ let interp_search_notation ?loc tag okey =
Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
end; ntn
| [ntn] ->
- Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+ Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
| ntns' ->
let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
@@ -297,7 +297,7 @@ let interp_search_notation ?loc tag okey =
let rbody = glob_constr_of_notation_constr ?loc body in
let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
- Feedback.msg_info (hov 0 m) in
+ Feedback.msg_notice (hov 0 m) in
if List.length !scs > 1 then
let scs' = List.remove (=) sc !scs in
let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
@@ -464,7 +464,7 @@ let interp_modloc mr =
let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
- Feedback.msg_info (hov 2 pr_res ++ fnl ())
+ Feedback.msg_notice (hov 2 pr_res ++ fnl ())
}
@@ -559,7 +559,7 @@ END
let print_view_hints env sigma kind l =
let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
- Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
+ Feedback.msg_notice (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
}
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 67f49f0074..0b465418f2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -220,13 +220,13 @@ let tclLOG (dbg,_,depth,trace) pp tac =
tac >>= fun v ->
tclENV >>= fun env ->
tclEVARMAP >>= fun sigma ->
- Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
+ Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
tclUNIT v
) tclUNIT
(fun (exn, info) ->
tclENV >>= fun env ->
tclEVARMAP >>= fun sigma ->
- Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
+ Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
tclZERO ~info exn))
| Info ->
(* For "info (trivial/auto)", we store a log trace *)
@@ -260,19 +260,19 @@ let pr_info_atom env sigma (d,pp) =
let pr_info_trace env sigma = function
| (Info,_,_,{contents=(d,Some pp)::l}) ->
- Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
+ Feedback.msg_notice (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
- | (Info,_,_,_) -> Feedback.msg_info (str "idtac.")
+ | (Info,_,_,_) -> Feedback.msg_notice (str "idtac.")
| _ -> ()
let pr_dbg_header = function
| (Off,_,_,_) -> ()
- | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
- | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
- | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)")
- | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)")
+ | (Debug,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* debug trivial: *)")
+ | (Debug,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* debug auto: *)")
+ | (Info,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* info trivial: *)")
+ | (Info,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* info auto: *)")
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index d4e4322bef..2ce32b309a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -351,13 +351,13 @@ let mk_eauto_dbg d =
else Off
let pr_info_nop = function
- | Info -> Feedback.msg_info (str "idtac.")
+ | Info -> Feedback.msg_notice (str "idtac.")
| _ -> ()
let pr_dbg_header = function
| Off -> ()
- | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
- | Info -> Feedback.msg_info (str "(* info eauto: *)")
+ | Debug -> Feedback.msg_notice (str "(* debug eauto: *)")
+ | Info -> Feedback.msg_notice (str "(* info eauto: *)")
let pr_info dbg s =
if dbg != Info then ()
@@ -368,7 +368,7 @@ let pr_info dbg s =
| State sp ->
let mindepth = loop sp in
let indent = String.make (mindepth - sp.depth) ' ' in
- Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str ".");
+ Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str ".");
mindepth
in
ignore (loop s)
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index 2761b87b02..5e81b43504 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -2,18 +2,18 @@
simple apply or_intror (in core).
intro.
assumption.
-Debug: (* debug auto: *)
-Debug: * assumption. (*fail*)
-Debug: * intro. (*fail*)
-Debug: * simple apply or_intror (in core). (*success*)
-Debug: ** assumption. (*fail*)
-Debug: ** intro. (*success*)
-Debug: ** assumption. (*success*)
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* simple apply or_intror (in core). (*success*)
+** assumption. (*fail*)
+** intro. (*success*)
+** assumption. (*success*)
(* info eauto: *)
simple apply or_intror.
intro.
exact H.
-Debug: (* debug eauto: *)
+(* debug eauto: *)
Debug: 1 depth=5
Debug: 1.1 depth=4 simple apply or_intror
Debug: 1.1.1 depth=4 intro
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4ae9d6d54f..e2bfbf626a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2267,7 +2267,7 @@ let with_fail ~st f =
user_err ~hdr:"Fail" (str "The command has not failed!")
| Ok msg ->
if not !Flags.quiet || !test_mode
- then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+ then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg)
let locate_if_not_already ?loc (e, info) =
match Loc.get_loc info with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:29:54 +0000