diff options
| author | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
| commit | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (patch) | |
| tree | c4a4b20e92547abae487f8bb1115ba34382f0bfd /lib/flags.ml | |
| parent | 79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (diff) | |
| parent | 40ed1b7c5e94f418f9b758ffe1a86e4ad7743267 (diff) | |
Merge PR #9410: Make `Program` a regular attribute
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 6 |
1 files changed, 0 insertions, 6 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 |