diff options
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | lib/clib.mllib | 5 | ||||
| -rw-r--r-- | lib/pp.ml | 2 | ||||
| -rw-r--r-- | library/goptions.ml | 4 | ||||
| -rw-r--r-- | library/library.ml | 2 | ||||
| -rw-r--r-- | library/loadpath.ml | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | pretyping/matching.ml | 6 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 3 | ||||
| -rw-r--r-- | toplevel/command.ml | 4 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/locality.ml | 3 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 2 |
18 files changed, 25 insertions, 28 deletions
diff --git a/checker/check.ml b/checker/check.ml index 267fdb886..0d8a4cd22 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -177,7 +177,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - Flags.if_warn msg_warning + msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); diff --git a/checker/check.mllib b/checker/check.mllib index 2671788b4..48c629009 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -4,8 +4,8 @@ Option Store Exninfo Backtrace -Pp_control Flags +Pp_control Pp Loc Segmenttree diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7edb52072..339a01d97 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1004,7 +1004,7 @@ let alias_of = function | (id::_,_) -> Name id let message_redundant_alias (id1,id2) = - if_warn msg_warning + msg_warning (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) (** {6 Expanding notations } diff --git a/interp/notation.ml b/interp/notation.ml index d0b4651ec..9bbaf9d86 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -182,7 +182,7 @@ let declare_delimiters scope key = | None -> scope_map := Gmap.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - Flags.if_warn msg_warning + msg_warning (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); scope_map := Gmap.add scope newsc !scope_map end; @@ -190,7 +190,7 @@ let declare_delimiters scope key = let oldscope = Gmap.find key !delimiters_map in if String.equal oldscope scope then () else begin - Flags.if_warn msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); + msg_warning (strbrk ("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 @@ -353,7 +353,7 @@ let declare_notation_interpretation ntn scopt pat df = | None -> "" | Some _ -> " in scope " ^ scope in let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in - Flags.if_warn msg_warning (strbrk message) + msg_warning (strbrk message) in let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in let () = scope_map := Gmap.add scope sc !scope_map in diff --git a/lib/clib.mllib b/lib/clib.mllib index a9b596b99..022a14ac3 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,3 +1,5 @@ +Coq_config + Int Option Store @@ -5,8 +7,8 @@ Exninfo Backtrace IArray Pp_control +Flags Pp -Coq_config Deque Hashset Hashcons @@ -18,6 +20,5 @@ Util Loc Serialize Xml_utils -Flags CUnix Envars @@ -341,7 +341,7 @@ let std_logger level msg = match level with | Debug _ -> msgnl (debugbody msg) (* cyan *) | Info -> msgnl (print_color "37" (hov 0 msg)) (* gray *) | Notice -> msgnl msg -| Warning -> msgnl_with !err_ft (warnbody msg) (* bright yellow *) +| Warning -> Flags.if_warn (msgnl_with !err_ft) (warnbody msg) (* bright yellow *) | Error -> msgnl_with !err_ft (errorbody msg) (* bright red *) let logger = ref std_logger diff --git a/library/goptions.ml b/library/goptions.ml index 597c23b7d..80539a156 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -314,12 +314,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_warn msg_warning s + with UserError (_,s) -> 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_warn msg_warning s + with UserError (_,s) -> 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 e1ef4515d..52d3a5d1d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -424,7 +424,7 @@ 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_warn msg_warning + msg_warning (pr_dirpath m.library_name ++ str " is already loaded from file " ++ str (library_full_filename m.library_name)); m.library_name, [] diff --git a/library/loadpath.ml b/library/loadpath.ml index 873703aff..60799a8a7 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -74,7 +74,7 @@ let add_load_path phys_path isroot coq_path = begin (* Assume the user is concerned by library naming *) if not (DirPath.equal dir Nameops.default_root_prefix) then - Flags.if_warn msg_warning + msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); diff --git a/library/nametab.ml b/library/nametab.ml index 12cad7f55..9f2bede75 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -120,7 +120,6 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Flags.if_warn msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path @@ -160,7 +159,6 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Flags.if_warn msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 8f34ec495..24ce7d652 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 - Flags.if_warn msg_warning + 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 " ++ diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c0c20a1e3..fa7b954d9 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_warn msg_warning (strbrk "Ignoring recursive call"); + msg_warning (strbrk "Ignoring recursive call"); (None,rest) | _ -> (None, rest)) in diff --git a/pretyping/matching.ml b/pretyping/matching.ml index ab90b5601..b3dc790e0 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -57,7 +57,7 @@ let constrain n (ids, m as x) (names, terms as subst) = with Not_found -> if List.mem_assoc n names then - Flags.if_warn Pp.msg_warning + msg_warning (str "Collision between bound variable " ++ pr_id n ++ str " and a metavariable of same name."); (names,(n,x)::terms) @@ -66,12 +66,12 @@ 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_warn Pp.msg_warning + (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_warn Pp.msg_warning + Pp.msg_warning (str "Collision between bound variable " ++ pr_id id1 ++ str " and another bound variable of same name."); ((id1,id2)::names,terms)); diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d227e1f2a..5e4e5eb97 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -330,8 +330,7 @@ let rec pat_of_raw metas vars = function | GHole _ -> PMeta None | GCast (_,c,_) -> - Flags.if_warn - Pp.msg_warning (strbrk "Cast not taken into account in constr pattern"); + Pp.msg_warning (strbrk "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 1071605fc..9267e236d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -147,7 +147,7 @@ let declare_definition ident (local, k) ce imps hook = let () = if Pfedit.refining () then let msg = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals" in - Flags.if_warn msg_warning msg + msg_warning msg in VarRef ident | Discharge | Local | Global -> @@ -503,7 +503,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_warn msg_warning (non_full_mutual_message x xge y yge isfix rest) + 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 bed262bbb..8551c2038 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -138,7 +138,7 @@ let alarm what internal msg = | KernelVerbose | KernelSilent -> (if debug then - Flags.if_warn Pp.msg_warning + msg_warning (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) | _ -> errorlabstrm "" msg diff --git a/toplevel/locality.ml b/toplevel/locality.ml index 49478cb26..6ee0e99b0 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -32,8 +32,7 @@ let enforce_locality_full locality_flag local = Errors.error "Use only prefix \"Local\"." | None -> if local then begin - Flags.if_warn - Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix."); + Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix."); Some true end else None diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 266397de8..1909f6809 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -164,7 +164,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.Id.of_string d with UserError _ -> - if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); raise Exit let add_rec_path ~unix_path ~coq_root = |