diff options
| author | Gaëtan Gilbert | 2018-11-13 16:02:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-26 13:21:56 +0100 |
| commit | ec209ea02cb8fa86f09aff88d0464c865ed7b8a5 (patch) | |
| tree | d9e28d57d4127fe08acaff4f730b2ec5cbc4cb17 /toplevel | |
| parent | b400fa987dec3c2dabfd69ce305d3ab8f1dc8952 (diff) | |
Put -indices-matter in typing_flags
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
3 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 15411d55d0..4d2b657b3c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -64,6 +64,7 @@ type coq_cmdopts = { color : color; impredicative_set : Declarations.set_predicativity; + indices_matter : bool; enable_VM : bool; enable_native_compiler : bool; stm_flags : Stm.AsyncOpts.stm_opt; @@ -118,6 +119,7 @@ let init_args = { color = `AUTO; impredicative_set = Declarations.PredicativeSet; + indices_matter = false; enable_VM = true; enable_native_compiler = Coq_config.native_compiler; stm_flags = Stm.AsyncOpts.default_opts; @@ -565,7 +567,7 @@ let parse_args arglist : coq_cmdopts * string list = |"-filteropts" -> { oval with filter_opts = true } |"-impredicative-set" -> { oval with impredicative_set = Declarations.ImpredicativeSet } - |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval + |"-indices-matter" -> { oval with indices_matter = true } |"-m"|"--memory" -> { oval with memory_stat = true } |"-noinit"|"-nois" -> { oval with load_init = false } |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index b709788dde..18ab6c3153 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -43,6 +43,7 @@ type coq_cmdopts = { color : color; impredicative_set : Declarations.set_predicativity; + indices_matter : bool; enable_VM : bool; enable_native_compiler : bool; stm_flags : Stm.AsyncOpts.stm_opt; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 66af7f7cdf..1b72a9554e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -435,6 +435,7 @@ let init_toplevel custom_init arglist = Flags.if_verbose print_header (); Mltop.init_known_plugins (); Global.set_engagement opts.impredicative_set; + Global.set_indices_matter opts.indices_matter; Global.set_VM opts.enable_VM; Global.set_native_compiler opts.enable_native_compiler; |