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/flags.mli | |
| 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/flags.mli')
| -rw-r--r-- | lib/flags.mli | 4 |
1 files changed, 0 insertions, 4 deletions
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 |