diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 14:46:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 14:46:37 +0200 |
| commit | 429f493997e34bfaac930c68bf6b267a5b9640ee (patch) | |
| tree | 28f15d0aeff2ce899a312f31e10fe2030b2dd813 /toplevel/coqtop.ml | |
| parent | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff) | |
| parent | eaa3f9719d6190ba92ce55816f11c70b30434309 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 22ab469dc..1544fd869 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -135,9 +135,9 @@ let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_include d p recursive implicit = +let set_include d p implicit = let p = dirpath_of_string p in - push_include d p recursive implicit + push_include d p implicit let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -402,21 +402,21 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: "-as" :: p :: rem -> set_include d p false true; args := rem - | d :: "-as" :: [] -> error_missing_arg "-as" | d :: rem -> push_ml_include d; args := rem | [] -> error_missing_arg opt end |"-Q" -> begin match rem with - | d :: p :: rem -> set_include d p true false; args := rem + | d :: p :: rem -> set_include d p false; args := rem | _ -> error_missing_arg opt end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg "-as" - | d :: "-as" :: p :: rem - | d :: p :: rem -> set_include d p true true; args := rem + | 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 |