diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.mli | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 4 |
3 files changed, 9 insertions, 1 deletions
diff --git a/lib/envars.mli b/lib/envars.mli index edd13447fc..18b7676ce7 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -53,7 +53,7 @@ val coqroot : string the order it gets added to the search path. *) val coqpath : string list -(** [camlbin ()] is the path to the ocamlfind binary. *) +(** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string (** [camlp4bin ()] is the path to the camlp4 binary. *) diff --git a/lib/flags.ml b/lib/flags.ml index 13539bced3..46bbba8e55 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -163,6 +163,10 @@ let use_polymorphic_flag () = let make_polymorphic_flag b = local_polymorphic_flag := Some b +let inductive_cumulativity = ref false +let make_inductive_cumulativity b = inductive_cumulativity := b +let is_inductive_cumulativity () = !inductive_cumulativity + (** [program_mode] tells that Program mode has been activated, either globally via [Set Program] or locally via the Program command prefix. *) diff --git a/lib/flags.mli b/lib/flags.mli index 0026aba2e3..5e78f0a041 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,6 +119,10 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool +(** Global inductive cumulativity flag. *) +val make_inductive_cumulativity : bool -> unit +val is_inductive_cumulativity : unit -> bool + val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit |