diff options
| author | Emilio Jesus Gallego Arias | 2018-08-20 17:29:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-20 17:29:53 +0200 |
| commit | 8a9c8f66a8c92ceb54e5325418c1a2074a7e4c6c (patch) | |
| tree | 361e91bc97ee1eff71370a5095c09d094217e5d0 /toplevel | |
| parent | c66c27781c555ec7301300cbf0d0342394c03981 (diff) | |
| parent | 066d6c657f6bf292969a58cd85cc5650721e5103 (diff) | |
Merge PR #8262: Remove dead argument allow_old.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 900964609d..113ba3684c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -425,7 +425,7 @@ let parse_args arglist : coq_cmdopts * string list = |"-worker-id" -> set_worker_id opt (next ()); oval |"-compat" -> - let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in + let v = G_vernac.parse_compat_version (next ()) in Flags.compat_version := v; add_compat_require oval v |