diff options
| author | Maxime Dénès | 2019-01-25 17:47:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-05 09:36:51 +0100 |
| commit | 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 (patch) | |
| tree | e6697a39eb0cfb7b45a08e88dd08ad2fe7eedadb /lib | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
Make Program a regular attribute
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 4 |
2 files changed, 0 insertions, 10 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 55bfa3cbde..29406ef275 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -107,12 +107,6 @@ let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity -(** [program_mode] tells that Program mode has been activated, either - globally via [Set Program] or locally via the Program command prefix. *) - -let program_mode = ref false -let is_program_mode () = !program_mode - let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x diff --git a/lib/flags.mli b/lib/flags.mli index 7336b9beaf..b9c5e20f47 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,10 +77,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Miscellaneus flags for vernac *) -val program_mode : bool ref -val is_program_mode : unit -> bool - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool |