diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 | ||||
| -rw-r--r-- | man/coqide.1 | 8 | ||||
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
7 files changed, 3 insertions, 18 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 076519dc6..0f4bb342a 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -178,11 +178,6 @@ The following command-line options are recognized by the commands {\tt Cause \Coq~not to load the resource file. -\item[{\tt -user} {\em username}]\ - - Take resource file of user {\em username} (that is - \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours. - \item[{\tt -load-ml-source} {\em file}]\ Load the Caml source file {\em file}. diff --git a/man/coqide.1 b/man/coqide.1 index 20379ef4d..9862ebb25 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -12,11 +12,11 @@ coqide \- The Coq Proof Assistant graphical interface .SH DESCRIPTION -.B coqtop +.B coqide is a gtk graphical interface for the Coq proof assistant. For command-line-oriented use of Coq, see -.BR coqide (1) +.BR coqtop (1) ; for batch-oriented use of Coq, see .BR coqc (1). @@ -112,10 +112,6 @@ Skip loading of rcfile. Set the rcfile to .IR f . .TP -.BI \-user\ u -Use the rcfile of user -.IR u . -.TP .B \-batch Batch mode (exits just after arguments parsing). .TP diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 688f7c32a..dfcb9c188 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -131,7 +131,7 @@ let parse_args () = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-outputstate"|"-inputstate"|"-is" |"-load-vernac-source"|"-l"|"-load-vernac-object" - |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" + |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem -> begin match rem with diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 7d178ede3..d77122892 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -21,7 +21,6 @@ let set_debug () = Flags.debug := true let rcfile = ref (Envars.xdg_config_home/"coqrc") let rcfile_specified = ref false let set_rcfile s = rcfile := s; rcfile_specified := true -let set_rcuser s = rcfile := ("~"^s)^"/.config/coq/coqrc" let load_rc = ref true let no_load_rc () = load_rc := false diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 7fda9544b..43b1556d5 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -11,7 +11,6 @@ val set_debug : unit -> unit val set_rcfile : string -> unit -val set_rcuser : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6d342b7ca..76e9c2fef 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -270,9 +270,6 @@ let parse_args arglist = | "-init-file" :: f :: rem -> set_rcfile f; parse rem | "-init-file" :: [] -> usage () - | "-user" :: u :: rem -> set_rcuser u; parse rem - | "-user" :: [] -> usage () - | "-notactics" :: rem -> warning "Obsolete option \"-notactics\"."; remove_top_ml (); parse rem diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 512632316..8c9b10786 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -53,7 +53,6 @@ let print_usage_channel co command = \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -\n -user u use the rcfile of user u\ \n -batch batch mode (exits just after arguments parsing)\ \n -boot boot mode (implies -q and -batch)\ \n -emacs tells Coq it is executed under Emacs\ |