diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2aad417e8..bd0a79caf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -443,10 +443,6 @@ let parse_args arglist = end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg opt - | d :: "-as" :: p :: rem -> - warning "option -R * -as * deprecated, remove the -as"; - set_include d p true; args := rem | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end |