aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/command.ml3
-rw-r--r--vernac/lemmas.ml5
-rw-r--r--vernac/metasyntax.ml7
-rw-r--r--vernac/mltop.ml3
-rw-r--r--vernac/vernacentries.ml25
5 files changed, 19 insertions, 24 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index 32ab5401a..b611edc41 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -9,7 +9,6 @@
open Pp
open CErrors
open Util
-open Flags
open Term
open Vars
open Termops
@@ -692,7 +691,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
constrimpls)
impls;
let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
- if_verbose Feedback.msg_info (minductive_message warn_prim names);
+ Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names);
if mie.mind_entry_private == None
then declare_default_schemes mind;
mind
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c60..590fa6213 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,7 +11,6 @@
open CErrors
open Util
-open Flags
open Pp
open Names
open Term
@@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+ Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c424b1d50..7b0d59812 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Flags
open CErrors
open Util
open Names
@@ -794,7 +793,7 @@ type notation_modifier = {
(* common to syn_data below *)
only_parsing : bool;
only_printing : bool;
- compat : compat_version option;
+ compat : Flags.compat_version option;
format : string Loc.located option;
extra : (string * string) list;
}
@@ -1073,7 +1072,7 @@ module SynData = struct
(* Fields coming from the vernac-level modifiers *)
only_parsing : bool;
only_printing : bool;
- compat : compat_version option;
+ compat : Flags.compat_version option;
format : string Loc.located option;
extra : (string * string) list;
@@ -1389,7 +1388,7 @@ let add_notation_interpretation ((loc,df),c,sc) =
let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
- (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index e8a0ba3dd..1edbd1a85 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
open Pp
-open Flags
open Libobject
open System
@@ -365,7 +364,7 @@ let trigger_ml_object verb cache reinit ?path name =
else begin
let file = file_of_name (Option.default name path) in
let path =
- if_verbose_load (verb && not !quiet) load_ml_object name ?path file in
+ if_verbose_load (verb && not !Flags.quiet) load_ml_object name ?path file in
add_loaded_module name (Some path);
if cache then perform_cache_obj name
end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fd08b42d..b0e438a8e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -11,7 +11,6 @@
open Pp
open CErrors
open Util
-open Flags
open Names
open Nameops
open Term
@@ -657,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
id binders_ast (Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -678,7 +677,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
export id binders_ast mty_ast_o
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Interactive Module " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -696,7 +695,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
id binders_ast mty_ast_o mexpr_ast_l
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
@@ -704,7 +703,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let vernac_end_module export (loc,id as lid) =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
- if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident lid]) export
let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -725,7 +724,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign
in
Dumpglob.dump_moddef ?loc mp "modtype";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Interactive Module Type " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -744,13 +743,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign mty_ast_l
in
Dumpglob.dump_moddef ?loc mp "modtype";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref ?loc mp "modtype";
- if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_include l =
Declaremods.declare_include Modintern.interp_module_ast l
@@ -818,7 +817,7 @@ let vernac_coercion locality poly local ref qids qidt =
let source = cl_of_qualid qids in
let ref' = smart_global ref in
Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
- if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
+ Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion locality poly local id qids qidt =
let local = enforce_locality locality local in
@@ -920,7 +919,7 @@ let vernac_chdir = function
so we make it an error. *)
user_err Pp.(str ("Cd failed: " ^ err))
end;
- if_verbose Feedback.msg_info (str (Sys.getcwd()))
+ Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
(********************)
@@ -1302,7 +1301,7 @@ let _ =
optname = "automatic introduction of variables";
optkey = ["Automatic";"Introduction"];
optread = Flags.is_auto_intros;
- optwrite = make_auto_intros }
+ optwrite = Flags.make_auto_intros }
let _ =
declare_bool_option
@@ -2050,7 +2049,7 @@ let interp ?proof ?loc locality poly c =
| VernacSearch (s,g,r) -> vernac_search ?loc s g r
| VernacLocate l -> vernac_locate l
| VernacRegister (id, r) -> vernac_register id r
- | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
+ | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
@@ -2176,7 +2175,7 @@ let with_fail b f =
| HasNotFailed ->
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
- if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info
+ if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 04:47:56 +0000