aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml4
-rw-r--r--interp/topconstr.ml2
-rw-r--r--kernel/univ.ml2
-rw-r--r--lib/pp.ml41
-rw-r--r--lib/pp.mli2
-rw-r--r--library/library.ml2
-rw-r--r--plugins/xml/cic2acic.ml4
-rw-r--r--plugins/xml/xmlcommand.ml26
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--printing/printer.ml4
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/tacinterp.ml4
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/metasyntax.ml4
-rw-r--r--toplevel/mltop.ml42
-rw-r--r--toplevel/obligations.ml2
-rw-r--r--toplevel/vernacentries.ml2
20 files changed, 35 insertions, 40 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 44a77836c..7ea55d833 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -68,8 +68,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try id_of_string d
with _ ->
- if_verbose warning
- ("Directory "^d^" cannot be used as a Coq identifier (skipped)");
+ if_verbose msg_warning
+ (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
flush_all ();
failwith "caught"
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 824b7f59a..1036baf7c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -138,7 +138,7 @@ let fold_constr_expr_with_binders g f n acc = function
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (loc,_,_) ->
- Pp.warning "Capture check in multiple binders not done"; acc
+ msg_warning (str "Capture check in multiple binders not done"); acc
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index a6942ea88..2384fdd55 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -172,7 +172,7 @@ let type0_univ = Atom UniverseLevel.Set
let is_type0_univ = function
| Atom UniverseLevel.Set -> true
- | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true
+ | Max ([UniverseLevel.Set], []) -> msg_warning (str "Non canonical Set"); true
| u -> false
let is_univ_variable = function
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index ff1973846..0a3466859 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -321,7 +321,6 @@ let pperr x = pp_with !err_ft x
let pperrnl x = ppnl_with !err_ft x
let message s = ppnl (str s)
let warning x = warning_with !err_ft x
-let warn x = warn_with !err_ft x
let pp_flush x = Format.pp_print_flush !std_ft x
let flush_all() = flush stderr; flush stdout; pp_flush()
diff --git a/lib/pp.mli b/lib/pp.mli
index 112d97655..da37a1153 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -101,8 +101,6 @@ val ppnl : std_ppcmds -> unit
val pperr : std_ppcmds -> unit
val pperrnl : std_ppcmds -> unit
val message : string -> unit (** = pPNL *)
-val warning : string -> unit
-val warn : std_ppcmds -> unit
val pp_flush : unit -> unit
val flush_all: unit -> unit
diff --git a/library/library.ml b/library/library.ml
index 66bca4f1b..417c567a8 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -656,7 +656,7 @@ let save_library_to dir f =
System.marshal_out ch di;
System.marshal_out ch table;
close_out ch
- with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
+ with e -> msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f'; raise e
(************************************************************************)
(*s Display the memory use of a library. *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index ec0910d7f..e29fcd0e8 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -23,8 +23,8 @@ let get_module_path_of_full_path path =
(function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
with
[] ->
- Pp.warning ("Modules not supported: reference to "^
- Libnames.string_of_path path^" will be wrong");
+ Pp.msg_warning (Pp.str ("Modules not supported: reference to "^
+ Libnames.string_of_path path^" will be wrong"));
dirpath
| [modul] -> modul
| _ ->
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 81dba546e..ee9bcb25d 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -426,46 +426,46 @@ let kind_of_constant kn =
| IsAssumption Definitional -> "AXIOM","Declaration"
| IsAssumption Logical -> "AXIOM","Axiom"
| IsAssumption Conjectural ->
- Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
+ Pp.msg_warning (Pp.str "Conjecture not supported in dtd (used Declaration instead)");
"AXIOM","Declaration"
| IsDefinition Definition -> "DEFINITION","Definition"
| IsDefinition Example ->
- Pp.warning "Example not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Example not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition Coercion ->
- Pp.warning "Coercion not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Coercion not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition SubClass ->
- Pp.warning "SubClass not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "SubClass not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition CanonicalStructure ->
- Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "CanonicalStructure not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition Fixpoint ->
- Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Fixpoint not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition CoFixpoint ->
- Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "CoFixpoint not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition Scheme ->
- Pp.warning "Scheme not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Scheme not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition StructureComponent ->
- Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "StructureComponent not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition IdentityCoercion ->
- Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "IdentityCoercion not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition Instance ->
- Pp.warning "Instance not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Instance not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsDefinition Method ->
- Pp.warning "Method not supported in dtd (used Definition instead)";
+ Pp.msg_warning (Pp.str "Method not supported in dtd (used Definition instead)");
"DEFINITION","Definition"
| IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) ->
"THEOREM",Kindops.string_of_theorem_kind thm
| IsProof _ ->
- Pp.warning "Unsupported theorem kind (used Theorem instead)";
+ Pp.msg_warning (Pp.str "Unsupported theorem kind (used Theorem instead)");
"THEOREM",Kindops.string_of_theorem_kind Theorem
;;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fd20f199c..a3fe0d059 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -490,7 +490,7 @@ and share_names isgoal n l avoid env c t =
share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
(* If built with the f/n notation: we renounce to share names *)
| _ ->
- if n>0 then warning "Detyping.detype: cannot factorize fix enough";
+ if n>0 then msg_warning (str "Detyping.detype: cannot factorize fix enough");
let c = detype isgoal avoid env c in
let t = detype isgoal avoid env t in
(List.rev l,c,t)
diff --git a/printing/printer.ml b/printing/printer.ml
index 1c51a6755..54e78a716 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -480,7 +480,7 @@ let pr_prim_rule = function
(str"fix " ++ pr_id f ++ str"/" ++ int n)
| FixRule (f,n,others,j) ->
- if j<>0 then warning "Unsupported printing of \"fix\"";
+ if j<>0 then msg_warning (str "Unsupported printing of \"fix\"");
let rec print_mut = function
| (f,n,ar)::oth ->
pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -492,7 +492,7 @@ let pr_prim_rule = function
(str"cofix " ++ pr_id f)
| Cofix (f,others,j) ->
- if j<>0 then warning "Unsupported printing of \"fix\"";
+ if j<>0 then msg_warning (str "Unsupported printing of \"fix\"");
let rec print_mut = function
| (f,ar)::oth ->
(pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6146998cb..404516279 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -518,7 +518,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty)
else begin
if not eapply then failwith "make_apply_entry";
if verbose then
- warn (str "the hint: eapply " ++ pr_lconstr c ++
+ msg_warning (str "the hint: eapply " ++ pr_lconstr c ++
str " will only be used by eauto");
(Some hd,
{ pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d98167ed0..0bcc4ed47 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -235,7 +235,7 @@ let add_tactic s t =
let overwriting_add_tactic s t =
if Hashtbl.mem tac_tab s then begin
Hashtbl.remove tac_tab s;
- warning ("Overwriting definition of tactic "^s)
+ msg_warning (str ("Overwriting definition of tactic "^s))
end;
Hashtbl.add tac_tab s t
@@ -273,7 +273,7 @@ let lookup_genarg id =
try Gmap.find id !extragenargtab
with Not_found ->
let msg = "No interpretation function found for entry " ^ id in
- warning msg;
+ msg_warning (str msg);
let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in
add_interp_genarg id f;
f
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 4c267ca83..ad2eb69b4 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -261,7 +261,7 @@ let add_new_coercion_core coef stre source target isid =
in
check_source (Some cls);
if not (uniform_cond (llp-ind) lvs) then
- warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform));
+ msg_warning (explain_coercion_error coef NotUniform);
let clt =
try
get_target tg ind
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 51d66a761..12ce73a5b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -91,7 +91,7 @@ let interp_definition bl red_option c ctypopt =
let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
(* Check that all implicit arguments inferable from the term is inferable from the type *)
if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false)
- then warn (str "Implicit arguments declaration relies on type." ++
+ then msg_warning (str "Implicit arguments declaration relies on type." ++
spc () ++ str "The term declares more implicits than the type here.");
imps1@(Impargs.lift_implicits nb_args impsty),
{ const_entry_body = body;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3936d2e80..2bc4fa97c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -123,8 +123,8 @@ let compile_files () =
let set_compat_version = function
| "8.3" -> compat_version := Some V8_3
| "8.2" -> compat_version := Some V8_2
- | "8.1" -> warning "Compatibility with version 8.1 not supported."
- | "8.0" -> warning "Compatibility with version 8.0 not supported."
+ | "8.1" -> msg_warning (str "Compatibility with version 8.1 not supported.")
+ | "8.0" -> msg_warning (str "Compatibility with version 8.0 not supported.")
| s -> error ("Unknown compatibility version \""^s^"\".")
(*s options for the virtual machine *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 3fba117a9..8804c60c8 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -272,7 +272,7 @@ let declare_congr_scheme ind =
then
ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
else
- warning "Cannot build congruence scheme because eq is not found"
+ msg_warning (str "Cannot build congruence scheme because eq is not found")
end
let declare_sym_scheme ind =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e98aa8c26..fe7394e94 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -846,7 +846,7 @@ let check_rule_productivity l =
error "A recursive notation must start with at least one symbol."
let is_not_printable = function
- | NVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
+ | NVar _ -> msg_warning (str "This notation will not be used for printing as it is bound to a single variable."); true
| _ -> false
let find_precedence lev etyps symbols =
@@ -904,7 +904,7 @@ let remove_curly_brackets l =
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
if l <> l0 or l' <> l1 then
- warning "Skipping spaces inside curly brackets";
+ msg_warning (str "Skipping spaces inside curly brackets");
if deb & l'' = [] then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index e02e6329d..2256d1b1d 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -117,7 +117,7 @@ let dir_ml_load s =
let dir_ml_use s =
match !load with
| WithTop t -> t.use_file s
- | _ -> warning "Cannot access the ML compiler"
+ | _ -> msg_warning (str "Cannot access the ML compiler")
(* Adds a path to the ML paths *)
let add_ml_dir s =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 5ca9ac9b4..61cc6b348 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -300,7 +300,6 @@ let safe_init_constant md name () =
let fix_proto = safe_init_constant tactics_module "fix_proto"
let hide_obligation = safe_init_constant tactics_module "obligation"
-let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Errors.errorlabstrm "Program" cmd
let error s = pperror (str s)
@@ -736,7 +735,6 @@ let not_transp_msg =
str "Obligation should be transparent but was declared opaque." ++ spc () ++
str"Use 'Defined' instead."
-let warn_not_transp () = ppwarn not_transp_msg
let error_not_transp () = pperror not_transp_msg
let rec string_of_list sep f = function
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2d3886a1d..dd8f1cd0e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -739,7 +739,7 @@ let vernac_chdir = function
| Some path ->
begin
try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
- with Sys_error str -> warning ("Cd failed: " ^ str)
+ with Sys_error err -> msg_warning (str ("Cd failed: " ^ err))
end;
if_verbose message (Sys.getcwd())
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 04:11:42 +0000