diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 142f3386..e9e86953 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 = @@ -378,7 +378,7 @@ let schedule_vio_compilation () = let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try - String.concat Filename.dir_sep [Filename.dirname s; + String.concat "/" [Filename.dirname s; Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" @@ -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 |