Merge PR #7851: Modernize the introduction of the reference manual.

3 files changed, 52 insertions, 37 deletions

diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 3e988709c..3574bf675 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -3,6 +3,21 @@
 @String{lnai  = "Lecture Notes in Artificial Intelligence"}
 @String{SV    = "{Sprin-ger-Verlag}"}
 
+@InCollection{Asp00,
+  Title        = {Proof General: A Generic Tool for Proof Development},
+  Author       = {Aspinall, David},
+  Booktitle    = {Tools and Algorithms for the Construction and
+               Analysis of Systems, {TACAS} 2000},
+  Publisher    = {Springer Berlin Heidelberg},
+  Year         = {2000},
+  Editor       = {Graf, Susanne and Schwartzbach, Michael},
+  Pages        = {38--43},
+  Series       = {Lecture Notes in Computer Science},
+  Volume       = {1785},
+  Doi          = {10.1007/3-540-46419-0_3},
+  ISBN         = {978-3-540-67282-1},
+}
+
 @Book{Bar81,
   author      = {H.P. Barendregt},
   publisher   = {North-Holland},
@@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}},
   year        = {1995}
 }
 
-@Misc{Pcoq,
-  author      = {Lemme Team},
-  title       = {Pcoq a graphical user-interface for {Coq}},
-  note        = {\url{http://www-sop.inria.fr/lemme/pcoq/}}
-}
-
-@Misc{ProofGeneral,
-  author      = {David Aspinall},
-  title       = {Proof General},
-  note        = {\url{https://proofgeneral.github.io/}}
+@InProceedings{Pit16,
+  Title        = {Company-Coq: Taking Proof General one step closer to a real IDE},
+  Author       = {Pit-Claudel, Clément and Courtieu, Pierre},
+  Booktitle    = {CoqPL'16: The Second International Workshop on Coq for PL},
+  Year         = {2016},
+  Month        = jan,
+  Doi          = {10.5281/zenodo.44331},
 }
 
 @Book{RC95,
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index f3ae49381..baf2e0d98 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -84,3 +84,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the
 terms and conditions set forth in the Open Publication License, v1.0 or later
 (the latest version is presently available at
 http://www.opencontent.org/openpub). Options A and B are not elected.
+
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+         Optionally, you can enhance it with the minor mode
+         Company-Coq :cite:`Pit16`
+         (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index bc72877b6..c7bc69db4 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -28,37 +28,35 @@ programs called *tactics*.
 All services of the |Coq| proof assistant are accessible by interpretation
 of a command language called *the vernacular*.
 
-Coq has an interactive mode in which commands are interpreted as the
+Coq has an interactive mode in which commands are interpreted as the
 user types them in from the keyboard and a compiled mode where commands
 are processed from a file.
 
--  The interactive mode may be used as a debugging mode in which the
-   user can develop his theories and proofs step by step, backtracking
-   if needed and so on. The interactive mode is run with the `coqtop` 
-   command from the operating system (which we shall assume to be some
-   variety of UNIX in the rest of this document).
+-  In interactive mode, users can develop their theories and proofs step by
+   step, and query the system for available theorems and definitions. The
+   interactive mode is generally run with the help of an IDE, such
+   as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`,
+   Emacs with Proof-General :cite:`Asp00` [#PG]_,
+   or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq).
+   The `coqtop` read-eval-print-loop can also be used directly, for debugging
+   purposes.
 
 -  The compiled mode acts as a proof checker taking a file containing a
    whole development in order to ensure its correctness. Moreover,
    |Coq|’s compiler provides an output file containing a compact
    representation of its input. The compiled mode is run with the `coqc`
-   command from the operating system.
+   command.
 
-These two modes are documented in Chapter :ref:`thecoqcommands`.
-
-Other modes of interaction with |Coq| are possible: through an emacs shell
-window, an emacs generic user-interface for proof assistant (Proof
-General :cite:`ProofGeneral`) or through a customized
-interface (PCoq :cite:`Pcoq`). These facilities are not
-documented here. There is also a |Coq| Integrated Development Environment
-described in :ref:`coqintegrateddevelopmentenvironment`.
+.. seealso:: :ref:`thecoqcommands`.
 
 How to read this book
 =====================
 
-This is a Reference Manual, not a User Manual, so it is not made for a
-continuous reading. However, it has some structure that is explained
-below.
+This is a Reference Manual, so it is not made for a continuous reading.
+We recommend using the various indexes to quickly locate the documentation
+you are looking for. There is a global index, and a number of specific indexes
+for tactics, vernacular commands, and error messages and warnings.
+Nonetheless, the manual has some structure that is explained below.
 
 -  The first part describes the specification language, |Gallina|.
    Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete
@@ -68,7 +66,7 @@ below.
    of the formalism. Chapter :ref:`themodulesystem` describes the module
    system.
 
--  The second part describes the proof engine. It is divided in five
+-  The second part describes the proof engine. It is divided in six
    chapters. Chapter :ref:`vernacularcommands` presents all commands (we
    call them *vernacular commands*) that are not directly related to
    interactive proving: requests to the environment, complete or partial
@@ -79,24 +77,24 @@ below.
    *tactics*. The language to combine these tactics into complex proof
    strategies is given in Chapter :ref:`ltac`. Examples of tactics
    are described in Chapter :ref:`detailedexamplesoftactics`.
+   Finally, the |SSR| proof language is presented in
+   Chapter :ref:`thessreflectprooflanguage`.
 
--  The third part describes how to extend the syntax of |Coq|. It
-   corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`.
+-  The third part describes how to extend the syntax of |Coq| in
+   Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define
+   new induction principles in Chapter :ref:`proofschemes`.
 
 -  In the fourth part more practical tools are documented. First in
    Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and
    `coqtop` (interactive mode) with their options is described. Then,
    in Chapter :ref:`utilities`, various utilities that come with the
    |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` 
-   describes the |Coq| integrated development environment.
+   describes CoqIDE.
 
 -  The fifth part documents a number of advanced features, including coercions,
    canonical structures, typeclasses, program extraction, and specialized
    solvers and tactics. See the table of contents for a complete list.
 
-At the end of the document, after the global index, the user can find
-specific indexes for tactics, vernacular commands, and error messages.
-
 List of additional documentation
 ================================
 
@@ -109,5 +107,5 @@ Installation
 
 The |Coq| standard library
     A commented version of sources of the |Coq| standard library
-    (including only the specifications, the proofs are removed) is given
-    in the additional document `Library.ps`.
+    (including only the specifications, the proofs are removed) is
+    available at https://coq.inria.fr/stdlib/.