From 3930c586507bfb3b80297d7a2fdbbc6049aa509b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Sep 2015 19:13:30 +0200
Subject: Updating the documentation and the toolchain w.r.t. the change in
 -compile.

---
 doc/refman/RefMan-com.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6335dfd324..2f9758fdee 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -162,11 +162,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
     Require} {\em file}).
 
-\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ 
+\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
   {\tt coqtop} options only used internally by {\tt coqc}.
 
-  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a
+  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
   copy of the contents of the file on standard input.  This option implies options
   {\tt -batch} (exit just after arguments parsing). It is only
   available for {\tt coqtop}.
-- 
cgit v1.2.3


From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Sep 2015 12:25:35 +0200
Subject: The -require option now accepts a logical path instead of a physical
 one.

---
 doc/refman/RefMan-com.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 2f9758fdee..0f1823a021 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -157,10 +157,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   Load \Coq~compiled file {\em file}{\tt .vo}
 
-\item[{\tt -require} {\em file}]\ 
+\item[{\tt -require} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
-    Require} {\em file}).
+  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
+    Require Import} {\em path}).
 
 \item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
-- 
cgit v1.2.3


From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Sep 2015 11:04:59 +0200
Subject: Make -load-vernac-object respect the loadpath.

This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.

This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
---
 doc/refman/RefMan-com.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 0f1823a021..9862abb533 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
   standard input.
 
-\item[{\tt -load-vernac-object} {\em file}]\ 
+\item[{\tt -load-vernac-object} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo}
+  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
 
 \item[{\tt -require} {\em path}]\ 
 
-- 
cgit v1.2.3


From ab3a1aed8fcaed3b0988b686b7f4cf7124b07ab2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 11 Dec 2015 12:15:17 +0100
Subject: Remove Set Virtual Machine from doc, since the command itself has
 been removed.

---
 doc/refman/RefMan-com.tex | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 9862abb533..8bb1cc331b 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -87,7 +87,6 @@ code. The list of highlight tags can be retrieved with the {\tt -list-tags}
 command-line option of {\tt coqtop}.
 
 \subsection{By command line options\index{Options of the command line}
-\label{vmoption}
 \label{coqoptions}}
 
 The following command-line options are recognized by the commands {\tt
@@ -224,11 +223,6 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
 \item[{\tt -no-hash-consing}] \mbox{}
 
-\item[{\tt -vm}]\ 
-
-  This activates the use of the bytecode-based conversion algorithm
-  for the current session (see Section~\ref{SetVirtualMachine}).
-
 \item[{\tt -image} {\em file}]\ 
 
   This option sets the binary image to be used by {\tt coqc} to be {\em file}
-- 
cgit v1.2.3


From 905e3dd364e8be20771c39393e7e114f2e4b8cd8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 6 Jan 2016 16:26:04 +0100
Subject: Fix description of command-line options in the manual.

---
 doc/refman/RefMan-com.tex | 225 +++++++++++++++++++++++++++-------------------
 1 file changed, 132 insertions(+), 93 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8bb1cc331b..6f85849888 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -5,9 +5,9 @@
 
 There are three \Coq~commands: 
 \begin{itemize}
-\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
-\item {\tt coqc} : The \Coq\ compiler (batch compilation).
-\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
+\item {\tt coqtop}: the \Coq\ toplevel (interactive mode);
+\item {\tt coqc}: the \Coq\ compiler (batch compilation);
+\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries).
 \end{itemize}
 The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the \verb!man! pages of
@@ -39,11 +39,10 @@ The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 
-\Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the Section~\ref{lexical}. It
-must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+.
+\Warning The name {\em file} should be a regular {\Coq} identifier, as
+defined in Section~\ref{lexical}. It should contain only letters, digits
+or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but
+\verb+/bar/foo/to-to.v+ is invalid.
 
 \section[Customization]{Customization at launch time}
 
@@ -64,7 +63,7 @@ directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
-\section{By environment variables\label{EnvVariables}
+\subsection{By environment variables\label{EnvVariables}
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
@@ -93,13 +92,13 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ %
 
-Add physical path {\em directory} to the {\ocaml} loadpath.
+  Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
 
-\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+\item[{\tt -Q} {\em directory} {\dirpath}]\ %
 
   Add physical path \emph{directory} to the list of directories where
   {\Coq} looks for a file and bind it to the the logical directory
@@ -109,147 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -R} {\em directory} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}]\ %
 
   Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
   subdirectory structure of \emph{directory} recursively visible so
   that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
-  
+
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
+\item[{\tt -top} {\dirpath}]\ %
+
+  Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not
+  valid for {\tt coqc} as the toplevel module name is inferred from the
+  name of the output file.
+
+\item[{\tt -notop}]\ %
+
+  Use the empty logical path for the toplevel module name instead of {\tt
+    Top}. Not valid for {\tt coqc} as the toplevel module name is
+  inferred from the name of the output file.
+
+\item[{\tt -exclude-dir} {\em directory}]\ %
 
-  This sets the toplevel module name to {\dirpath}/the empty logical path instead
-  of {\tt Top}. Not valid for {\tt coqc}.
+  Exclude any subdirectory named {\em directory} while
+  processing options such as {\tt -R} and {\tt -Q}. By default, only the
+  conventional version control management directories named {\tt CVS} and
+  {\tt \_darcs} are excluded.
 
-\item[{\tt -exclude-dir} {\em subdirectory}]\ 
+\item[{\tt -nois}]\ %
 
-  This tells to exclude any subdirectory named {\em subdirectory}
-  while processing option {\tt -R}. Without this option only the
-  conventional version control management subdirectories named {\tt
-  CVS} and {\tt \_darcs} are excluded.
+  Start from an empty state instead of loading the {\tt Init.Prelude}
+  module.
 
-\item[{\tt -nois}]\ 
+\item[{\tt -init-file} {\em file}]\ %
 
-  Cause \Coq~to begin with an empty state.
+  Load {\em file} as the resource file instead of loading the default
+  resource file from the standard configuration directories.
 
-\item[{\tt -init-file} {\em file}, {\tt -q}]\ 
+\item[{\tt -q}]\ %
 
-  Take {\em file} as the resource file. /
-  Cause \Coq~not to load the resource file.
+  Do not to load the default resource file.
 
-\item[{\tt -load-ml-source} {\em file}]\ 
+\item[{\tt -load-ml-source} {\em file}]\ %
 
   Load the {\ocaml} source file {\em file}.
 
-\item[{\tt -load-ml-object} {\em file}]\ 
+\item[{\tt -load-ml-object} {\em file}]\ %
 
   Load the {\ocaml} object file {\em file}.
 
-\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ 
+\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+
+\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em
+    file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+  Output its content on the standard input as it is executed.
+
+\item[{\tt -load-vernac-object} {\dirpath}]\ %
+
+  Load \Coq~compiled library {\dirpath}. This is equivalent to running
+  {\tt Require} {\dirpath}.
 
-  Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
-  standard input.
+\item[{\tt -require} {\dirpath}]\ %
 
-\item[{\tt -load-vernac-object} {\em path}]\ 
+  Load \Coq~compiled library {\dirpath} and import it. This is equivalent
+  to running {\tt Require Import} {\dirpath}.
 
-  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
+\item[{\tt -batch}]\ %
 
-\item[{\tt -require} {\em path}]\ 
+  Exit just after argument parsing. Available for {\tt coqtop} only.
 
-  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
-    Require Import} {\em path}).
+\item[{\tt -compile} {\em file.v}]\ %
 
-\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
+  Compile file {\em file.v} into {\em file.vo}. This options imply {\tt
+    -batch} (exit just after argument parsing). It is available only
+  for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}.
 
-  {\tt coqtop} options only used internally by {\tt coqc}.
+\item[{\tt -compile-verbose} {\em file.v}]\ %
 
-  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
-  copy of the contents of the file on standard input.  This option implies options
-  {\tt -batch} (exit just after arguments parsing). It is only
-  available for {\tt coqtop}.
+  Same as {\tt -compile} but also output the content of {\em file.v} as
+  it is compiled.
 
-\item[{\tt -verbose}]\ 
+\item[{\tt -verbose}]\ %
 
-  This option is only for {\tt coqc}. It tells to compile the file with
-  a copy of its contents on standard input.
+  Output the content of the input file as it is compiled. This option is
+  available for {\tt coqc} only; it is the counterpart of {\tt
+    -compile-verbose}.
 
 %Mostly unused in the code
-%\item[{\tt -debug}]\ 
+%\item[{\tt -debug}]\ %
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ 
+\item[{\tt -with-geoproof} (yes|no)]\ %
 
-  Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
+  Enable or not special functions for Geoproof within {\CoqIDE} (default
+  is yes).
 
-\item[{\tt -color} (on|off|auto)]\
+\item[{\tt -color} (on|off|auto)]\ %
 
-  Activate or not the coloring of output of {\tt coqtop}. The default, auto,
-  means that {\tt coqtop} will dynamically decide whether to activate it
-  depending if the output channels of {\tt coqtop} can handle ANSI styles.
+  Enable or not the coloring of output of {\tt coqtop}. Default is auto,
+  meaning that {\tt coqtop} dynamically decides, depending on whether the
+  output channel supports ANSI escape sequences.
 
-\item[{\tt -beautify}]\ 
+\item[{\tt -beautify}]\ %
 
-  While compiling {\em file}, pretty prints each command just after having parsing
-  it in {\em file}{\tt .beautified} in order to get old-fashion
-  syntax/definitions/notations.
+  Pretty-print each command to {\em file.beautified} when compiling {\em
+    file.v}, in order to get old-fashioned syntax/definitions/notations.
 
-\item[{\tt -emacs}, {\tt -ide-slave}]\ 
+\item[{\tt -emacs}, {\tt -ide-slave}]\ %
 
-  Start a special main loop to communicate with ide.
+  Start a special toplevel to communicate with a specific IDE.
 
-\item[{\tt -impredicative-set}]\ 
+\item[{\tt -impredicative-set}]\ %
 
   Change the logical theory of {\Coq} by declaring the sort {\tt Set}
-  impredicative; warning: this is known to be inconsistent with
+  impredicative. Warning: this is known to be inconsistent with
   some standard axioms of classical mathematics such as the functional
-  axiom of choice or the principle of description
+  axiom of choice or the principle of description.
 
-\item[{\tt -type-in-type}]\
+\item[{\tt -type-in-type}]\ %
 
-  This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+  Collapse the universe hierarchy of {\Coq}. Warning: this makes the
+  logic inconsistent.
 
-\item[{\tt -compat} {\em version}] \mbox{}
+\item[{\tt -compat} {\em version}]\ %
 
-  Attempt to maintain some of the incompatible changes in their {\em version}
-  behavior.
+  Attempt to maintain some backward-compatibility with a previous version.
 
-\item[{\tt -dump-glob} {\em file}]\ 
+\item[{\tt -dump-glob} {\em file}]\ %
 
-  This dumps references for global names in file {\em file}
-  (to be used by coqdoc, see~\ref{coqdoc})
+  Dump references for global names in file {\em file} (to be used
+  by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being
+  compiled, {\em file.glob} is used.
 
-\item[{\tt -no-hash-consing}] \mbox{}
+\item[{\tt -no-glob}]\ %
 
-\item[{\tt -image} {\em file}]\ 
+  Disable the dumping of references for global names.
 
-  This option sets the binary image to be used by {\tt coqc} to be {\em file}
+%\item[{\tt -no-hash-consing}]\ %
+
+\item[{\tt -image} {\em file}]\ %
+
+  Set the binary image to be used by {\tt coqc} to be {\em file}
   instead of the standard one. Not of general use.
 
-\item[{\tt -bindir} {\em directory}]\ 
+\item[{\tt -bindir} {\em directory}]\ %
+
+  Set the directory containing {\Coq} binaries to be used by {\tt coqc}.
+  It is equivalent to doing \texttt{export COQBIN=}{\em directory} before
+  launching {\tt coqc}.
+
+\item[{\tt -where}]\ %
+
+  Print the location of \Coq's standard library and exit.
 
-  Set for {\tt coqc} the directory containing \Coq\ binaries.
-  It is equivalent to do \texttt{export COQBIN=}{\em directory}
-  before launching {\tt coqc}.
+\item[{\tt -config}]\ %
 
-\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ 
+  Print the locations of \Coq's binaries, dependencies, and libraries, then exit.
 
-  Print the \Coq's standard library location or \Coq's binaries, dependencies,
-  libraries locations or the list of command line arguments that {\tt coqtop} has
-  recognize as options and exit.
+\item[{\tt -filteropts}]\ %
 
-\item[{\tt -v}]\ 
+  Print the list of command line arguments that {\tt coqtop} has
+  recognized as options and exit.
 
-  Print the \Coq's version and exit.
+\item[{\tt -v}]\ %
 
-\item[{\tt -list-tags}]\
+  Print \Coq's version and exit.
 
-  Print the highlight tags known by \Coq as well as their currently associated
-  color.
+\item[{\tt -list-tags}]\ %
 
-\item[{\tt -h}, {\tt --help}]\ 
+  Print the highlight tags known by {\Coq} as well as their currently associated
+  color and exit.
+
+\item[{\tt -h}, {\tt --help}]\ %
 
   Print a short usage and exit.
 
@@ -293,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
 same meaning as for {\tt coqtop}. Extra options are:
 \begin{description}
-\item[{\tt -norec} $module$]\ 
+\item[{\tt -norec} {\em module}]\ %
+
+  Check {\em module} but do not check its dependencies.
 
-  Check $module$ but do not force check of its dependencies.
-\item[{\tt -admit} $module$] \
+\item[{\tt -admit} {\em module}]\ %
 
-  Do not check $module$ and any of its dependencies, unless
+  Do not check {\em module} and any of its dependencies, unless
   explicitly required.
-\item[{\tt -o}]\ 
+
+\item[{\tt -o}]\ %
 
   At exit, print a summary about the context. List the names of all
   assumptions and variables (constants without body).
-\item[{\tt -silent}]\ 
+
+\item[{\tt -silent}]\ %
 
   Do not write progress information in standard output.
 \end{description}
-- 
cgit v1.2.3

