aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml2
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml6
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--plugins/extraction/g_extraction.ml44
-rw-r--r--plugins/extraction/table.ml18
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/firstorder/ground.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml8
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/merge.ml14
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/micromega/coq_micromega.ml22
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/rtauto/proof_search.ml2
-rw-r--r--plugins/rtauto/refl_tauto.ml12
-rw-r--r--plugins/setoid_ring/g_newring.ml48
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--plugins/syntax/nat_syntax.ml2
23 files changed, 71 insertions, 71 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 898dcd255..76db2f3c2 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
let cc_verbose=ref false
let debug x =
- if !cc_verbose then msg_debug (x ())
+ if !cc_verbose then Feedback.msg_debug (x ())
let _=
let gdopt=
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c8924073c..bd788a425 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms =
List.map
(build_term_to_complete uf newmeta)
(epsilons uf) in
- Pp.msg_info
+ Feedback.msg_info
(Pp.str "Goal is solvable by congruence but \
some arguments are missing.");
- Pp.msg_info
+ Feedback.msg_info
(Pp.str " Try " ++
hov 8
begin
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index be6ce59bd..3fa600ac2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -169,7 +169,7 @@ let do_daimon () =
daimon_instr env p
end
in
- if not status then Pp.feedback Feedback.AddedAxiom else ()
+ if not status then Feedback.feedback Feedback.AddedAxiom else ()
(* post-instruction focus management *)
@@ -291,7 +291,7 @@ let justification tac gls=
error "Insufficient justification."
else
begin
- msg_warning (str "Insufficient justification.");
+ Feedback.msg_warning (str "Insufficient justification.");
daimon_tac gls
end) gls
@@ -1293,7 +1293,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
end;
match bro with
None ->
- msg_warning (str "missing case");
+ Feedback.msg_warning (str "missing case");
tacnext (mkMeta 1)
| Some (sub_ids,tree) ->
let br_args =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 67c1c5901..a03be5743 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -541,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
(if dry then None else si);
(* Print the buffer content via Coq standard formatter (ok with coqide). *)
if not (Int.equal (Buffer.length buf) 0) then begin
- Pp.msg_notice (str (Buffer.contents buf));
+ Feedback.msg_notice (str (Buffer.contents buf));
Buffer.reset buf
end
@@ -635,7 +635,7 @@ let simple_extraction r =
in
let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
reset ();
- Pp.msg_notice ans
+ Feedback.msg_notice ans
| _ -> assert false
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index eb2f02244..0a8cb0ccd 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -101,7 +101,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> [ msg_info (print_extraction_inline ()) ]
+ -> [Feedback. msg_info (print_extraction_inline ()) ]
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -123,7 +123,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> [ msg_info (print_extraction_blacklist ()) ]
+ -> [ Feedback.msg_info (print_extraction_blacklist ()) ]
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f336941ee..560fe5aea 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -300,7 +300,7 @@ let warning_axioms () =
if List.is_empty info_axioms then ()
else begin
let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
- msg_warning
+ Feedback.msg_warning
(str ("The following "^s^" must be realized in the extracted code:")
++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
++ str "." ++ fnl ())
@@ -310,7 +310,7 @@ let warning_axioms () =
else begin
let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
in
- msg_warning
+ Feedback.msg_warning
(str ("The following logical "^s^" encountered:") ++
hov 1
(spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
@@ -326,12 +326,12 @@ let warning_opaques accessed =
else
let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
if accessed then
- msg_warning
+ Feedback.msg_warning
(str "The extraction is currently set to bypass opacity,\n" ++
str "the following opaque constant bodies have been accessed :" ++
lst ++ str "." ++ fnl ())
else
- msg_warning
+ Feedback.msg_warning
(str "The extraction now honors the opacity constraints by default,\n" ++
str "the following opaque constants have been extracted as axioms :" ++
lst ++ str "." ++ fnl () ++
@@ -339,7 +339,7 @@ let warning_opaques accessed =
++ fnl ())
let warning_both_mod_and_cst q mp r =
- msg_warning
+ Feedback.msg_warning
(str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
str "do you mean module " ++
pr_long_mp mp ++
@@ -358,7 +358,7 @@ let check_inside_module () =
err (str "You can't do that within a Module Type." ++ fnl () ++
str "Close it and try again.")
else if Lib.is_module () then
- msg_warning
+ Feedback.msg_warning
(str "Extraction inside an opened module is experimental.\n" ++
str "In case of problem, close it first.\n")
@@ -368,7 +368,7 @@ let check_inside_section () =
str "Close it and try again.")
let warning_id s =
- msg_warning (str ("The identifier "^s^
+ Feedback.msg_warning (str ("The identifier "^s^
" contains __ which is reserved for the extraction"))
let error_constant r =
@@ -449,7 +449,7 @@ let error_remaining_implicit k =
let warning_remaining_implicit k =
let s = msg_of_implicit k in
- msg_warning
+ Feedback.msg_warning
(str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
++ str "but this code is potentially unsafe, please review it manually.")
@@ -465,7 +465,7 @@ let check_loaded_modfile mp = match base_mp mp with
| _ -> ()
let info_file f =
- Flags.if_verbose msg_info
+ Flags.if_verbose Feedback.msg_info
(str ("The file "^f^" has been created by extraction."))
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 134b6ba94..a78532e33 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -74,7 +74,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> [
- Pp.msg_info
+ Feedback.msg_info
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
END
@@ -131,7 +131,7 @@ ARGUMENT EXTEND firstorder_using
| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
| [ "using" reference(a) reference(b) reference_list(l) ] -> [
Flags.if_verbose
- Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+ Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
a::b::l
]
| [ ] -> [ [] ]
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 3b9f67f66..d7da85b4f 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -32,7 +32,7 @@ let ground_tac solver startseq gl=
update_flags ();
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
- then Pp.msg_debug (Printer.pr_goal gl);
+ then Feedback.msg_debug (Printer.pr_goal gl);
tclORELSE (axiom_tac seq.gl seq)
begin
try
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 879145c2f..52094cf08 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -52,17 +52,17 @@ let rec print_debug_queue e =
let _ =
match e with
| Some e ->
- Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+ Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
| None ->
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
+ Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
end in
print_debug_queue None ;
end
let observe strm =
if do_observe ()
- then Pp.msg_debug strm
+ then Feedback.msg_debug strm
else ()
let do_observe_tac s tac g =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 91a826c73..5b4fb2595 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -19,7 +19,7 @@ exception Toberemoved
let observe s =
if do_observe ()
- then Pp.msg_debug s
+ then Feedback.msg_debug s
(*
Transform an inductive induction principle into
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6dfc23511..c63527dea 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -193,12 +193,12 @@ let warning_error names e =
let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
match e with
| Building_graph e ->
- Pp.msg_warning
+ Feedback.msg_warning
(str "Cannot define graph(s) for " ++
h 1 (pr_enum Libnames.pr_reference names) ++
if do_observe () then (spc () ++ Errors.print e) else mt ())
| Defining_principle e ->
- Pp.msg_warning
+ Feedback.msg_warning
(str "Cannot define principle(s) for "++
h 1 (pr_enum Libnames.pr_reference names) ++
if do_observe () then Errors.print e else mt ())
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8a0a1a064..72205e2bb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -14,7 +14,7 @@ open Misctypes
let observe strm =
if do_observe ()
- then Pp.msg_debug strm
+ then Feedback.msg_debug strm
else ()
(*let observennl strm =
if do_observe ()
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 84a4d910e..0cacb003d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -267,12 +267,12 @@ let derive_inversion fix_names =
lind;
with e when Errors.noncritical e ->
let e' = process_vernac_interp_error e in
- msg_warning
+ Feedback.msg_warning
(str "Cannot build inversion information" ++
if do_observe () then (fnl() ++ Errors.print e') else mt ())
with e when Errors.noncritical e ->
let e' = process_vernac_interp_error e in
- msg_warning
+ Feedback.msg_warning
(str "Cannot build inversion information (early)" ++
if do_observe () then (fnl() ++ Errors.print e') else mt ())
@@ -292,12 +292,12 @@ let warning_error names e =
in
match e with
| Building_graph e ->
- Pp.msg_warning
+ Feedback.msg_warning
(str "Cannot define graph(s) for " ++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
e_explain e)
| Defining_principle e ->
- Pp.msg_warning
+ Feedback.msg_warning
(str "Cannot define principle(s) for "++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
e_explain e)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 72529fbbe..94530bfde 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -53,7 +53,7 @@ let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds =
let observe strm =
if do_observe ()
- then Pp.msg_debug strm
+ then Feedback.msg_debug strm
else ()
(*let observennl strm =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c71d9a9ca..99a165044 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -504,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
| GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
- let _ = prstr "\nICI1!\n";Pp.flush_all() in
+ let _ = prstr "\nICI1!\n" in
let args = filter_shift_stable lnk (arr1 @ arr2) in
GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
| GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge
| GLetIn(_,nme,bdy,trm) , _ ->
- let _ = prstr "\nICI2!\n";Pp.flush_all() in
+ let _ = prstr "\nICI2!\n" in
let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
| _, GLetIn(_,nme,bdy,trm) ->
- let _ = prstr "\nICI3!\n";Pp.flush_all() in
+ let _ = prstr "\nICI3!\n" in
let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
- | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
+ | _ -> let _ = prstr "\nICI4!\n" in
raise NoMerge
let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
@@ -527,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
(* FIXME: what if the function appears in the body of the let? *)
| GLetIn(_,nme,bdy,trm) , _ ->
- let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
+ let _ = prstr "\nICI2 '!\n" in
let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
| _, GLetIn(_,nme,bdy,trm) ->
- let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
+ let _ = prstr "\nICI3 '!\n" in
let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
- | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
+ | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 10f08d3d1..80866e8b8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -214,17 +214,17 @@ let print_debug_queue b e =
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+ Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
else
begin
- Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
+ Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
end;
(* print_debug_queue false e; *)
end
let observe strm =
if do_observe ()
- then Pp.msg_debug strm
+ then Feedback.msg_debug strm
else ()
@@ -1537,7 +1537,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
with e when Errors.noncritical e ->
begin
if do_observe ()
- then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
+ then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
else anomaly (Pp.str "Cannot create equation Lemma")
;
true
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 0fcfbfc71..e4aa1448e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -961,7 +961,7 @@ struct
let parse_expr parse_constant parse_exp ops_spec env term =
if debug
- then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
+ then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
(*
let constant_or_variable env term =
@@ -1082,7 +1082,7 @@ struct
let rconstant term =
if debug
- then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
let res = rconstant term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1122,7 +1122,7 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
if debug
- then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
match kind_of_term cstr with
| App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
@@ -1651,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "Formula....\n") ;
+ Feedback.msg_notice (Pp.str "Formula....\n") ;
let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ Feedback.msg_notice (Printer.prterm ff);
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
match witness_list_tags prover cnf_ff with
@@ -1676,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "\nAFormula\n") ;
+ Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Feedback.msg_notice (Printer.prterm ff');
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
@@ -1733,7 +1733,7 @@ let micromega_gen
with
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound -> flush stdout ;
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1818,7 +1818,7 @@ let micromega_genr prover =
with
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound ->
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1903,7 +1903,7 @@ let call_csdpcert_q provername poly =
let cert = Certificate.q_cert_of_pos cert in
if Mc.qWeakChecker poly cert
then Some cert
- else ((print_string "buggy certificate" ; flush stdout) ;None)
+ else ((print_string "buggy certificate") ;None)
let call_csdpcert_z provername poly =
let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index dca46cbcf..007a9ec67 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -172,7 +172,7 @@ let print_env_reification env =
in
let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
- msg_debug (prop_info ++ fnl () ++ term_info)
+ Feedback.msg_debug (prop_info ++ fnl () ++ term_info)
(* \subsection{Gestion des environnements de variable pour Omega} *)
(* generation d'identifiant d'equation pour Omega *)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 3ba92b9f2..f3eae5f50 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -547,7 +547,7 @@ let pp_info () =
int s_info.created_branches ++ str " created" ++ fnl () ++
str "Hypotheses : " ++
int s_info.created_hyps ++ str " created" ++ fnl () in
- msg_info
+ Feedback.msg_info
( str "Proof-search statistics :" ++ fnl () ++
count_info ++
str "Branch ends: " ++
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 73dc13e72..0a0b45915 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -276,7 +276,7 @@ let rtauto_tac gls=
begin
reset_info ();
if !verbose then
- msg_info (str "Starting proof-search ...");
+ Feedback.msg_info (str "Starting proof-search ...");
end in
let search_start_time = System.get_time () in
let prf =
@@ -286,10 +286,10 @@ let rtauto_tac gls=
let search_end_time = System.get_time () in
let _ = if !verbose then
begin
- msg_info (str "Proof tree found in " ++
+ Feedback.msg_info (str "Proof tree found in " ++
System.fmt_time_difference search_start_time search_end_time);
pp_info ();
- msg_info (str "Building proof term ... ")
+ Feedback.msg_info (str "Building proof term ... ")
end in
let build_start_time=System.get_time () in
let _ = step_count := 0; node_count := 0 in
@@ -302,7 +302,7 @@ let rtauto_tac gls=
let build_end_time=System.get_time () in
let _ = if !verbose then
begin
- msg_info (str "Proof term built in " ++
+ Feedback.msg_info (str "Proof term built in " ++
System.fmt_time_difference build_start_time build_end_time ++
fnl () ++
str "Proof size : " ++ int !step_count ++
@@ -319,9 +319,9 @@ let rtauto_tac gls=
Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
let tac_end_time = System.get_time () in
let _ =
- if !check then msg_info (str "Proof term type-checking is on");
+ if !check then Feedback.msg_info (str "Proof term type-checking is on");
if !verbose then
- msg_info (str "Internal tactic executed in " ++
+ Feedback.msg_info (str "Internal tactic executed in " ++
System.fmt_time_difference tac_start_time tac_end_time) in
result
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index f5a734048..f64226e33 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -60,9 +60,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
add_theory id (ic t) set k cst (pre,post) power sign div]
| [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
- msg_notice (strbrk "The following ring structures have been declared:");
+ Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
- msg_notice (hov 2
+ Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr fi.ring_carrier++spc()++
str"and equivalence relation "++ pr_constr fi.ring_req))
@@ -89,9 +89,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
- msg_notice (strbrk "The following field structures have been declared:");
+ Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
- msg_notice (hov 2
+ Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr fi.field_carrier++spc()++
str"and equivalence relation "++ pr_constr fi.field_req))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 271bf35a8..154ec6e1b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -527,7 +527,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
let op_morph =
op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
Flags.if_verbose
- msg_info
+ Feedback.msg_info
(str"Using setoid \""++pr_constr req++str"\""++spc()++
str"and morphisms \""++pr_constr add_m_lem ++
str"\","++spc()++ str"\""++pr_constr mul_m_lem++
@@ -536,7 +536,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
op_morph)
| None ->
(Flags.if_verbose
- msg_info
+ Feedback.msg_info
(str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
str"and morphisms \""++pr_constr add_m_lem ++
str"\""++spc()++str"and \""++
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5f44904c3..fe9386039 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -25,7 +25,7 @@ let threshold = of_int 5000
let nat_of_int dloc n =
if is_pos_or_zero n then begin
if less_than threshold n then
- msg_warning
+ Feedback.msg_warning
(strbrk "Stack overflow or segmentation fault happens when " ++
strbrk "working with large numbers in nat (observed threshold " ++
strbrk "may vary from 5000 to 70000 depending on your system " ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-15 21:12:08 +0000