diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 470b7660b5b..389c2e13d05 100644 --- a/src/basic/FStarC.Options.fst +++ b/src/basic/FStarC.Options.fst @@ -1631,13 +1631,6 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d "locate_ocaml", Const (Bool true), text "Print the root of the built OCaml F* library and exit"); - ( noshort, - "ocamlenv", - WithSideEffect ((fun _ -> print_error "--ocamlenv must be the first argument, see fstar.exe --help for details\n"; exit 1), - (Const (Bool true))), - text "With no arguments: print an environment suitable for a shell (similar to 'opam env'). \ - With arguments: run a command in that environment. \ - NOTE: this must be the FIRST argument passed to F* and other options are NOT processed."); ] and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) = diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 5b236119e7b..b0245f4a8e8 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -113,28 +113,10 @@ let load_native_tactics () = (* print_in_place options are passed *) let fstar_files: ref (option (list string)) = Util.mk_ref None -(* ocamlenv mode: called whenever the *first* argument is exactly 'ocamlenv' *) -let go_ocamlenv rest_args = - let shellescape s = s in - let ocamldir = Find.locate_ocaml () in - let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in - let new_ocamlpath = ocamldir ^ ":" ^ old_ocamlpath in - match rest_args with - | [] -> - Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" (shellescape new_ocamlpath); - exit 0 - | cmd :: args -> - - Util.putenv "OCAMLPATH" new_ocamlpath; - Util.execvp cmd (cmd :: args) - | _ -> - let open FStarC.Pprint in - Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [ - Errors.Msg.text "Unrecognized usage of --ocamlenv"; - ] - -(* Normal mode with some flags, files, etc *) -let go_normal () = +(****************************************************************************) +(* Main function *) +(****************************************************************************) +let go _ = let res, filenames = process_args () in if Options.trace_error () then begin let h = get_sigint_handler () in @@ -303,17 +285,6 @@ let go_normal () = Errors.raise_error0 Errors.Error_MissingFileName "No file provided" end -(****************************************************************************) -(* Main function *) -(****************************************************************************) - -(* choose a main driver function and go *) -let go () = - let args = Util.get_cmd_args () in - match args with - | _ :: "--ocamlenv" :: rest -> go_ocamlenv rest - | _ -> go_normal () - (* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *) let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax.Syntax.term = match k with