aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/notation.ml8
-rw-r--r--library/goptions.ml4
-rw-r--r--library/library.ml6
-rw-r--r--library/nametab.ml14
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/matching.ml17
-rw-r--r--pretyping/pattern.ml4
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/lemmas.ml4
-rw-r--r--toplevel/mltop.ml44
-rw-r--r--toplevel/vernacexpr.ml2
14 files changed, 43 insertions, 42 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8dee1f0e0..b161d001d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -804,8 +804,8 @@ let alias_of = function
| (id::_,_) -> Name id
let message_redundant_alias (id1,id2) =
- if_verbose warning
- ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
+ if_warn msg_warning
+ (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
(* Expanding notations *)
@@ -933,7 +933,7 @@ let maybe_constructor ref f aliases env =
| InternalizationError _ -> VarPat (find_pattern_variable ref)
(* patt var also exists globally but does not satisfy preconditions *)
| (Environ.NotEvaluableConst _ | Not_found) ->
- if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
+ if_warn msg_warning (str "pattern " ++ pr_reference ref ++
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
diff --git a/interp/notation.ml b/interp/notation.ml
index aa35e4af0..9967a8e5e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -71,7 +71,7 @@ let init_scope_map () =
let declare_scope scope =
try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
-(* Flags.if_verbose message ("Creating scope "^scope);*)
+(* Flags.if_warn message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
@@ -151,15 +151,15 @@ let declare_delimiters scope key =
| None -> scope_map := Gmap.add scope newsc !scope_map
| Some oldkey when oldkey = key -> ()
| Some oldkey ->
- Flags.if_verbose warning
- ("overwriting previous delimiting key "^oldkey^" in scope "^scope);
+ Flags.if_warn msg_warning
+ (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
scope_map := Gmap.add scope newsc !scope_map
end;
try
let oldscope = Gmap.find key !delimiters_map in
if oldscope = scope then ()
else begin
- Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+ Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope));
delimiters_map := Gmap.add key scope !delimiters_map
end
with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
diff --git a/library/goptions.ml b/library/goptions.ml
index d882ed944..f5100a14a 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -335,12 +335,12 @@ let set_int_option_value_gen locality =
set_option_value locality check_int_value
let set_bool_option_value_gen locality key v =
try set_option_value locality check_bool_value key v
- with UserError (_,s) -> Flags.if_verbose msg_warning s
+ with UserError (_,s) -> Flags.if_warn msg_warning s
let set_string_option_value_gen locality =
set_option_value locality check_string_value
let unset_option_value_gen locality key =
try set_option_value locality check_unset_value key ()
- with UserError (_,s) -> Flags.if_verbose msg_warning s
+ with UserError (_,s) -> Flags.if_warn msg_warning s
let set_int_option_value = set_int_option_value_gen None
let set_bool_option_value = set_bool_option_value_gen None
diff --git a/library/library.ml b/library/library.ml
index 071c7a46c..376228748 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -463,9 +463,9 @@ let rec_intern_by_filename_only id f =
(* We check no other file containing same library is loaded *)
if library_is_loaded m.library_name then
begin
- Flags.if_verbose warning
- ((string_of_dirpath m.library_name)^" is already loaded from file "^
- library_full_filename m.library_name);
+ Flags.if_warn msg_warning
+ (pr_dirpath m.library_name ++ str " is already loaded from file " ++
+ str (library_full_filename m.library_name));
m.library_name, []
end
else
diff --git a/library/nametab.ml b/library/nametab.ml
index c6f04b016..6dbd927d8 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -108,9 +108,9 @@ struct
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- Flags.if_verbose
- warning ("Trying to mask the absolute name \""
- ^ U.to_string n ^ "\"!");
+ Flags.if_warn
+ msg_warning (str ("Trying to mask the absolute name \""
+ ^ U.to_string n ^ "\"!"));
current
| Nothing
| Relative _ -> Relative (uname,o)
@@ -131,7 +131,7 @@ struct
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
error ("Cannot mask the absolute name \""
- ^ U.to_string uname' ^ "\"!")
+ ^ U.to_string uname' ^ "\"!")
| Nothing
| Relative _ -> Absolute (uname,o), dirmap
@@ -148,9 +148,9 @@ let rec push_exactly uname o level (current,dirmap) = function
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- Flags.if_verbose
- warning ("Trying to mask the absolute name \""
- ^ U.to_string n ^ "\"!");
+ Flags.if_warn
+ msg_warning (str ("Trying to mask the absolute name \""
+ ^ U.to_string n ^ "\"!"));
current
| Nothing
| Relative _ -> Relative (uname,o)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b1e9f257f..ac81786b6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -130,14 +130,14 @@ END
let test_plurial_form = function
| [(_,([_],_))] ->
- Flags.if_verbose warning
- "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
+ Flags.if_verbose msg_warning
+ (str "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
| _ -> ()
let test_plurial_form_types = function
| [([_],_)] ->
- Flags.if_verbose warning
- "Keywords Implicit Types expect more than one type"
+ Flags.if_verbose msg_warning
+ (str "Keywords Implicit Types expect more than one type")
| _ -> ()
(* Gallina declarations *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b875912fc..a09760295 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -158,7 +158,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
(match dest_recarg ra with
| Mrec (_,j) when is_rec -> (depPvect.(j),rest)
| Imbr _ ->
- Flags.if_verbose warning "Ignoring recursive call";
+ Flags.if_warn msg_warning (str "Ignoring recursive call");
(None,rest)
| _ -> (None, rest))
in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 6e0ef5af1..7a7451187 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -7,6 +7,7 @@
(************************************************************************)
(*i*)
+open Pp
open Util
open Names
open Libnames
@@ -54,23 +55,23 @@ let constrain (n,(ids,m as x)) (names,terms as subst) =
with
Not_found ->
if List.mem_assoc n names then
- Flags.if_verbose Pp.warning
- ("Collision between bound variable "^string_of_id n^
- " and a metavariable of same name.");
+ Flags.if_warn Pp.msg_warning
+ (str "Collision between bound variable " ++ pr_id n ++
+ str " and a metavariable of same name.");
(names,(n,x)::terms)
let add_binders na1 na2 (names,terms as subst) =
match na1, na2 with
| Name id1, Name id2 ->
if List.mem_assoc id1 names then
- (Flags.if_verbose Pp.warning
- ("Collision between bound variables of name "^string_of_id id1);
+ (Flags.if_warn Pp.msg_warning
+ (str "Collision between bound variables of name " ++ pr_id id1);
(names,terms))
else
(if List.mem_assoc id1 terms then
- Flags.if_verbose Pp.warning
- ("Collision between bound variable "^string_of_id id1^
- " and another bound variable of same name.");
+ Flags.if_warn Pp.msg_warning
+ (str "Collision between bound variable " ++ pr_id id1 ++
+ str " and another bound variable of same name.");
((id1,id2)::names,terms));
| _ -> subst
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 585de58fb..65f342d88 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -300,8 +300,8 @@ let rec pat_of_raw metas vars = function
| GHole _ ->
PMeta None
| GCast (_,c,_) ->
- Flags.if_verbose
- Pp.warning "Cast not taken into account in constr pattern";
+ Flags.if_warn
+ Pp.msg_warning (str "Cast not taken into account in constr pattern");
pat_of_raw metas vars c
| GIf (_,c,(_,None),b1,b2) ->
PIf (pat_of_raw metas vars c,
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ffb1130eb..eca53ae71 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -118,7 +118,7 @@ let declare_definition ident (local,k) ce imps hook =
let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in
definition_message ident;
if Pfedit.refining () then
- Flags.if_verbose msg_warning
+ Flags.if_warn msg_warning
(str"Local definition " ++ pr_id ident ++
str" is not visible from current goals");
VarRef ident
@@ -445,7 +445,7 @@ let check_mutuality env isfix fixl =
let po = partial_order preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
| (x,Inr xge)::(y,Inr yge)::rest ->
- if_verbose msg_warning (non_full_mutual_message x xge y yge isfix rest)
+ if_warn msg_warning (non_full_mutual_message x xge y yge isfix rest)
| _ -> ()
type structured_fixpoint_expr = {
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index d346f422e..c92f63d09 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -128,7 +128,7 @@ let alarm what internal msg =
| KernelVerbose
| KernelSilent ->
(if debug then
- Flags.if_verbose Pp.msg_warning
+ Flags.if_warn Pp.msg_warning
(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
| _ -> errorlabstrm "" msg
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 6f344db58..7704449f5 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -124,13 +124,13 @@ let find_mutually_recursive_statements thms =
assert (rest=[]);
(* One occ. of common coind ccls and no common inductive hyps *)
if common_same_indhyp <> [] then
- if_verbose warning "Assuming mutual coinductive statements.";
+ if_verbose msgnl (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
if same_indccl <> [] &&
list_distinct (List.map pi1 (List.hd same_indccl)) then
- if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+ if_verbose msgnl (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
let possible_guards = List.map (List.map pi3) inds_hyps in
(* assume the largest indices as possible *)
list_last common_same_indhyp, false, possible_guards
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 3cda90425..ff3ce8a09 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -143,8 +143,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Names.id_of_string d
with _ ->
- if_verbose warning
- ("Directory "^d^" cannot be used as a Coq identifier (skipped)");
+ if_warn msg_warning
+ (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
flush_all ();
failwith "caught"
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index f2e2c0ac7..517d77e9d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -403,7 +403,7 @@ let enforce_locality_full local =
error "Use only prefix \"Local\"."
| None ->
if local then begin
- Flags.if_verbose
+ Flags.if_warn
Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
Some true
end else
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 11:55:04 +0000