aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml7
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat20
-rw-r--r--engine/eConstr.ml7
-rw-r--r--engine/universes.ml77
-rw-r--r--engine/universes.mli19
-rw-r--r--pretyping/classops.ml3
-rw-r--r--pretyping/reductionops.ml10
-rw-r--r--tactics/tactics.ml2
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--tools/coqc.ml2
-rw-r--r--toplevel/coqtop.ml40
-rw-r--r--toplevel/vernac.ml15
-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
17 files changed, 71 insertions, 176 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 7a69700d28..67b812133d 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open System
-open Flags
open Names
open Check
@@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Id.of_string d
with CErrors.UserError _ ->
- if_verbose Feedback.msg_warning
+ Flags.if_verbose Feedback.msg_warning
(str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
raise Exit
@@ -342,7 +341,7 @@ let parse_args argv =
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
- | "-boot" :: rem -> boot := true; parse rem
+ | "-boot" :: rem -> Flags.boot := true; parse rem
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
@@ -374,7 +373,7 @@ let init_with_argv argv =
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
- if_verbose print_header ();
+ Flags.if_verbose print_header ();
init_load_path ();
engage ();
with e ->
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index a420b5d8bb..f91b301b8c 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -328,12 +328,6 @@ ECHO ========== INSTALL CYGWIN ==========
REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
REM Otherwise chmod won't work and e.g. the ocaml build will fail.
REM Cygwin setup does not touch the ACLs of existing folders.
-REM => Create the setup log in a temporary location and move it later.
-
-REM Get Unique temporary file name
-:logfileloop
-SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log
-if exist "%LOGFILE%" GOTO logfileloop
REM Run Cygwin Setup
@@ -348,6 +342,12 @@ IF "%COQREGTESTING%" == "Y" (
SET RUNSETUP=Y
)
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+ SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5"
+)
+
IF "%RUNSETUP%"=="Y" (
%SETUP% ^
--proxy "%PROXY%" ^
@@ -356,10 +356,9 @@ IF "%RUNSETUP%"=="Y" (
--local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
--no-shortcuts ^
%CYGWIN_OPT% ^
- -P wget,curl,git,make,unzip ^
- -P gcc-core,gcc-g++ ^
+ -P make,unzip ^
-P gdb,liblzma5 ^
- -P patch,automake1.14,automake1.15 ^
+ -P patch,automake1.14 ^
-P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
@@ -369,12 +368,11 @@ IF "%RUNSETUP%"=="Y" (
-P gtk-update-icon-cache ^
-P libtool,automake ^
-P intltool ^
- > "%LOGFILE%" ^
+ %EXTRAPACKAGES% ^
|| GOTO ErrorExit
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
- MOVE "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit
)
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7b879a8031..a54c082979 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 =
let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
-(** TODO: factorize with universes.ml *)
let test_constr_universes sigma leq m n =
let open Universes in
let kind c = kind_upto sigma c in
@@ -574,14 +573,20 @@ let test_constr_universes sigma leq m n =
else
let cstrs = ref Constraints.empty in
let eq_universes strict l l' =
+ let l = EInstance.kind sigma (EInstance.make l) in
+ let l' = EInstance.kind sigma (EInstance.make l') in
cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
let eq_sorts s1 s2 =
+ let s1 = ESorts.kind sigma (ESorts.make s1) in
+ let s2 = ESorts.kind sigma (ESorts.make s2) in
if Sorts.equal s1 s2 then true
else (cstrs := Constraints.add
(Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
true)
in
let leq_sorts s1 s2 =
+ let s1 = ESorts.kind sigma (ESorts.make s1) in
+ let s2 = ESorts.kind sigma (ESorts.make s2) in
if Sorts.equal s1 s2 then true
else
(cstrs := Constraints.add
diff --git a/engine/universes.ml b/engine/universes.ml
index 719af43edf..686411e7d5 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -131,47 +131,6 @@ let to_constraints g s =
"to_constraints: non-trivial algebraic constraint between universes")
in Constraints.fold tr s Constraint.empty
-let test_constr_univs_infer leq univs fold m n accu =
- if m == n then Some accu
- else
- let cstrs = ref accu in
- let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let leq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let res =
- if leq then
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts
- eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
- else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- if res then Some !cstrs else None
-
-let eq_constr_univs_infer univs fold m n accu =
- test_constr_univs_infer false univs fold m n accu
-
-let leq_constr_univs_infer univs fold m n accu =
- test_constr_univs_infer true univs fold m n accu
-
(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
to expose subterms of [m] and [n], arguments. *)
let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
@@ -197,42 +156,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
if res then Some !cstrs else None
-let test_constr_universes leq m n =
- if m == n then Some Constraints.empty
- else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' =
- cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let leq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let res =
- if leq then
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
- else
- Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- if res then Some !cstrs else None
-
-let eq_constr_universes m n = test_constr_universes false m n
-let leq_constr_universes m n = test_constr_universes true m n
-
let compare_head_gen_proj env equ eqs eqc' m n =
match kind_of_term m, kind_of_term n with
| Proj (p, c), App (f, args)
diff --git a/engine/universes.mli b/engine/universes.mli
index fe40f82385..8b2217d446 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f
val to_constraints : UGraph.t -> universe_constraints -> constraints
-(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
- application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
- constr -> constr -> 'a -> 'a option
-
(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
{!eq_constr_univs_infer} taking kind-of-term functions, to expose
subterms of [m] and [n], arguments. *)
@@ -80,20 +75,6 @@ val eq_constr_univs_infer_with :
(constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
-(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
- modulo alpha, casts, application grouping, the universe constraints
- in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
- constr -> constr -> 'a -> 'a option
-
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
- application grouping and the universe constraints in [c]. *)
-val eq_constr_universes : constr -> constr -> universe_constraints option
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
- alpha, casts, application grouping and the universe constraints in [c]. *)
-val leq_constr_universes : constr -> constr -> universe_constraints option
-
(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and the universe constraints in [c]. *)
val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1cc072a2a2..260cd04446 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
open Pp
-open Flags
open Names
open Libnames
open Globnames
@@ -387,7 +386,7 @@ let add_coercion_in_graph (ic,source,target) =
old_inheritance_graph
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
- if is_ambig && not !quiet then
+ if is_ambig && not !Flags.quiet then
Feedback.msg_info (message_ambig !ambig_paths)
type coercion = {
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3563235434..2aa2f90131 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1438,17 +1438,13 @@ let sigma_univ_state =
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
(** FIXME *)
- let open Universes in
- let x = EConstr.Unsafe.to_constr x in
- let y = EConstr.Unsafe.to_constr y in
try
- let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in
let b, sigma =
let ans =
if pb == Reduction.CUMUL then
- Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+ EConstr.leq_constr_universes sigma x y
else
- Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+ EConstr.eq_constr_universes sigma x y
in
let ans = match ans with
| None -> None
@@ -1462,6 +1458,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
in
if b then sigma, true
else
+ let x = EConstr.Unsafe.to_constr x in
+ let y = EConstr.Unsafe.to_constr y in
let sigma' =
conv_fun pb ~l2r:false sigma ts
env (sigma, sigma_univ_state) x y in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5698312aef..d0165c555d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -74,7 +74,7 @@ let _ =
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "trigger bugged context matching compatibility";
optkey = ["Tactic";"Compat";"Context"];
optread = (fun () -> !Flags.tactic_context_compat) ;
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 56e12a1e06..afe8e62ee3 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -500,7 +500,7 @@ uninstall::
instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
rm -f "$$instf" &&\
echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \
+ (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
done
.PHONY: uninstall
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 862225d3d1..b381c5ba42 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -93,7 +93,7 @@ let parse_args () =
| ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
- |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
+ |"-q"|"-profile"|"-echo" |"-quiet"
|"-silent"|"-m"|"-beautify"|"-strict-implicit"
|"-impredicative-set"|"-vm"|"-native-compiler"
|"-indices-matter"|"-quick"|"-type-in-type"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0f8524e923..c1cdaa5a34 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -8,7 +8,6 @@
open Pp
open CErrors
-open Flags
open Libnames
open Coqinit
@@ -31,7 +30,7 @@ let print_header () =
Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
flush_all ()
-let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
+let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
let toploop = ref None
@@ -87,7 +86,7 @@ let console_toploop_run () =
(* We initialize the console only if we run the toploop_run *)
let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
if Dumpglob.dump () then begin
- if_verbose warning "Dumpglob cannot be used in interactive mode.";
+ Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
Coqloop.loop();
@@ -130,7 +129,7 @@ let set_type_in_type () =
let engage () =
Global.set_engagement !impredicative_set
-let set_batch_mode () = batch_mode := true
+let set_batch_mode () = Flags.batch_mode := true
let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
let toplevel_name = ref toplevel_default_name
@@ -177,7 +176,7 @@ let load_vernacular sid =
(fun sid (s,v) ->
let s = Loadpath.locate_file s in
if !Flags.beautify then
- with_option beautify_file (Vernac.load_vernac v sid) s
+ Flags.(with_option beautify_file (Vernac.load_vernac v sid) s)
else
Vernac.load_vernac v sid s)
sid (List.rev !load_vernacular_list)
@@ -199,7 +198,7 @@ let require_prelude () =
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- let () = if !load_init then silently require_prelude () in
+ let () = if !Flags.load_init then Flags.silently require_prelude () in
let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
@@ -229,7 +228,7 @@ let add_compile verbose s =
let compile_file (v,f) =
if !Flags.beautify then
- with_option beautify_file (Vernac.compile v) f
+ Flags.(with_option beautify_file (Vernac.compile v) f)
else
Vernac.compile v f
@@ -304,7 +303,7 @@ let usage () =
init_load_path ();
with NoCoqLib -> usage_no_coqlib ()
end;
- if !batch_mode then Usage.print_usage_coqc ()
+ if !Flags.batch_mode then Usage.print_usage_coqc ()
else begin
Mltop.load_ml_objects_raw_rex
(Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
@@ -538,7 +537,7 @@ let parse_args arglist =
|"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
- |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
+ |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo
|"-toploop" -> set_toploop (next ())
|"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ()))
|"-o" -> Flags.compilation_output_name := Some (next())
@@ -551,9 +550,9 @@ let parse_args arglist =
|"-async-proofs-never-reopen-branch" ->
Flags.async_proofs_never_reopen_branch := true;
|"-batch" -> set_batch_mode ()
- |"-test-mode" -> test_mode := true
- |"-beautify" -> beautify := true
- |"-boot" -> boot := true; no_load_rc ()
+ |"-test-mode" -> Flags.test_mode := true
+ |"-beautify" -> Flags.beautify := true
+ |"-boot" -> Flags.boot := true; no_load_rc ()
|"-bt" -> Backtrace.record_backtrace true
|"-color" -> set_color (next ())
|"-config"|"--config" -> print_config := true
@@ -565,19 +564,18 @@ let parse_args arglist =
|"-ideslave" -> set_ideslave ()
|"-impredicative-set" -> set_impredicative_set ()
|"-indices-matter" -> Indtypes.enforce_indices_matter ()
- |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
|"-m"|"--memory" -> memory_stat := true
- |"-noinit"|"-nois" -> load_init := false
+ |"-noinit"|"-nois" -> Flags.load_init := false
|"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
|"-native-compiler" ->
if Coq_config.no_native_compiler then
warning "Native compilation was disabled at configure time."
- else native_compiler := true
+ else Flags.native_compiler := true
|"-output-context" -> output_context := true
|"-profile-ltac" -> Flags.profile_ltac := true
|"-q" -> no_load_rc ()
|"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
- |"-quick" -> Flags.compilation_mode := BuildVio
+ |"-quick" -> Flags.compilation_mode := Flags.BuildVio
|"-list-tags" -> print_tags := true
|"-time" -> Flags.time := true
|"-type-in-type" -> set_type_in_type ()
@@ -620,11 +618,11 @@ let init_toplevel arglist =
prerr_endline "See -help for the list of supported options";
exit 1
end;
- if_verbose print_header ();
+ Flags.if_verbose print_header ();
inputstate ();
Mltop.init_known_plugins ();
engage ();
- if (not !batch_mode || CList.is_empty !compile_list)
+ if (not !Flags.batch_mode || CList.is_empty !compile_list)
&& Global.env_is_initial ()
then Declaremods.start_library !toplevel_name;
init_library_roots ();
@@ -645,16 +643,16 @@ let init_toplevel arglist =
with any ->
flush_all();
let extra =
- if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+ if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
then None
else Some (str "Error during initialization: ")
in
fatal_error ?extra any
end;
- if !batch_mode then begin
+ if !Flags.batch_mode then begin
flush_all();
if !output_context then
- Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
+ Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
Profile.print_profile ();
exit 0
end;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1602f9c683..c33f6b9b84 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -11,7 +11,6 @@
open Pp
open CErrors
open Util
-open Flags
open Vernacexpr
open Vernacprop
@@ -53,7 +52,7 @@ let set_formatter_translator ch =
let pr_new_syntax_in_context ?loc chan_beautify ocom =
let loc = Option.cata Loc.unloc (0,0) loc in
- if !beautify_file then set_formatter_translator chan_beautify;
+ if !Flags.beautify_file then set_formatter_translator chan_beautify;
let fs = States.freeze ~marshallable:`No in
(* The content of this is not supposed to fail, but if ever *)
try
@@ -63,7 +62,7 @@ let pr_new_syntax_in_context ?loc chan_beautify ocom =
| Some com -> Ppvernac.pr_vernac com
| None -> mt() in
let after = comment (CLexer.extract_comments (snd loc)) in
- if !beautify_file then
+ if !Flags.beautify_file then
(Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
Format.pp_print_flush !Topfmt.std_ft ())
else
@@ -209,7 +208,7 @@ and load_vernac verbosely sid file =
*)
in
(* Printing of vernacs *)
- if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+ if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
@@ -224,7 +223,7 @@ and load_vernac verbosely sid file =
match e with
| Stm.End_of_input ->
(* Is this called so comments at EOF are printed? *)
- if !beautify then
+ if !Flags.beautify then
pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
if !Flags.beautify_file then close_out chan_beautify;
!rsid
@@ -290,7 +289,7 @@ let compile verbosely f =
++ str ".")
in
match !Flags.compilation_mode with
- | BuildVo ->
+ | Flags.BuildVo ->
let long_f_dot_v = ensure_v f in
ensure_exists long_f_dot_v;
let long_f_dot_vo =
@@ -314,7 +313,7 @@ let compile verbosely f =
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
Dumpglob.end_dump_glob ()
- | BuildVio ->
+ | Flags.BuildVio ->
let long_f_dot_v = ensure_v f in
ensure_exists long_f_dot_v;
let long_f_dot_vio =
@@ -329,7 +328,7 @@ let compile verbosely f =
check_pending_proofs ();
Stm.snapshot_vio ldir long_f_dot_vio;
Stm.reset_task_queue ()
- | Vio2Vo ->
+ | Flags.Vio2Vo ->
let open Filename in
let open Library in
Dumpglob.noglob ();
diff --git a/vernac/command.ml b/vernac/command.ml
index 32ab5401a0..b611edc41d 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 645320c603..590fa62134 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 c424b1d501..7b0d59812c 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 e8a0ba3dda..1edbd1a850 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 4fd08b42d4..b0e438a8e3 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.25.1) at 2026-05-01 18:19:59 +0000