aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
7 files changed, 32 insertions, 37 deletions
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 ())
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:46:28 +0000