aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml17
1 files changed, 17 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 9b932946c..530617b0c 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -60,6 +60,8 @@ let async_proofs_is_worker () =
let debug = ref false
+let profile = false
+
let print_emacs = ref false
let term_quality = ref false
@@ -134,6 +136,21 @@ let auto_intros = ref true
let make_auto_intros flag = auto_intros := flag
let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
+let universe_polymorphism = ref false
+let make_universe_polymorphism b = universe_polymorphism := b
+let is_universe_polymorphism () = !universe_polymorphism
+
+let local_polymorphic_flag = ref None
+let use_polymorphic_flag () =
+ match !local_polymorphic_flag with
+ | Some p -> local_polymorphic_flag := None; p
+ | None -> is_universe_polymorphism ()
+let make_polymorphic_flag b =
+ local_polymorphic_flag := Some b
+
+(** [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