diff options
| author | Maxime Dénès | 2018-11-27 11:06:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-27 11:06:18 +0100 |
| commit | 31a1fa82bfc747df0c71c93346f689def876794a (patch) | |
| tree | fac54469054681647ab0659bdfeddcdb74eda4f9 /toplevel | |
| parent | 5fcf1b7dcd9b20ea7c5ad317ce2bfe4fbb5452d9 (diff) | |
| parent | ec209ea02cb8fa86f09aff88d0464c865ed7b8a5 (diff) | |
Merge PR #8986: 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 e3b15d1988..2f84eb9851 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; @@ -568,7 +570,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 a18da9c1e3..30f1caab12 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 5028f366cb..faacbe4c80 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -198,6 +198,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; |