aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml8
-rw-r--r--lib/flags.mli4
2 files changed, 0 insertions, 12 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02..eca9a69de 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -110,14 +110,6 @@ 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
-
let polymorphic_inductive_cumulativity = ref false
let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c..95916d3ab 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,10 +77,6 @@ val is_program_mode : unit -> bool
val make_universe_polymorphism : bool -> unit
val is_universe_polymorphism : unit -> bool
-(** Local universe polymorphism flag. *)
-val make_polymorphic_flag : bool -> unit
-val use_polymorphic_flag : unit -> bool
-
(** Global polymorphic inductive cumulativity flag. *)
val make_polymorphic_inductive_cumulativity : bool -> unit
val is_polymorphic_inductive_cumulativity : unit -> bool