Imported Upstream version 8.9.0upstream/8.9.0upstream

7 files changed, 239 insertions, 38 deletions

diff --git a/doc/LICENSE b/doc/LICENSE
index c223a4e1..3789d910 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -2,7 +2,7 @@ The Coq Reference Manual is a collective work from the Coq Development
 Team whose members are listed in the file CREDITS of the Coq source
 package. All related documents (the LaTeX and BibTeX sources, the
 embedded png files, and the PostScript, PDF and html outputs) are
-copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font
+copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font
 file UbuntuMono-B.ttf, which is
 Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font
 license, version 1.0
@@ -14,33 +14,14 @@ License, v1.0 or later (the latest version is presently available at
 http://www.opencontent.org/openpub/).  Options A and B are *not*
 elected.
 
-The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
-Paulin-Mohring. All documents (the LaTeX source and the PostScript,
-PDF and html outputs) are copyright (c) INRIA 1999-2006. The material
-connected to the Coq Tutorial 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.
-
 The Coq Standard Library is a collective work from the Coq Development
 Team whose members are listed in the file CREDITS of the Coq source
 package. All related documents (the Coq vernacular source files and
 the PostScript, PDF and html outputs) are copyright (c) INRIA
-1999-2006. The material connected to the Standard Library is
+1999-2018. The material connected to the Standard Library is
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
-Castéran and Eduardo Gimenez. All related documents (the LaTeX and
-BibTeX sources and the PostScript, PDF and html outputs) are copyright
-(c) INRIA 1997-2006. The material connected to the Tutorial on
-[Co-]Inductive Types in Coq 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.
-
 ----------------------------------------------------------------------
 
                       *Open Publication License*
diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 00000000..77fe617f
--- /dev/null
+++ b/doc/README.md
@@ -0,0 +1,126 @@
+The Coq documentation
+=====================
+
+The Coq documentation includes
+
+- A Reference Manual
+- A document presenting the Coq standard library
+
+The documentation of the latest released version is available on the Coq
+web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation).
+
+Additionally, you can view the documentation for the current master version at
+<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman>.
+
+The reference manual is written is reStructuredText and compiled
+using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst)
+to learn more about the format that is used.
+
+The documentation for the standard library is generated from
+the `.v` source files using coqdoc.
+
+Dependencies
+------------
+
+### HTML documentation
+
+To produce the complete documentation in HTML, you will need Coq dependencies
+listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based
+reference manual requires Python 3, and the following Python packages:
+
+  - sphinx
+  - sphinx_rtd_theme
+  - beautifulsoup4
+  - antlr4-python3-runtime
+  - pexpect
+  - sphinxcontrib-bibtex
+
+To install them, you should first install pip and setuptools (for instance,
+with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
+
+    pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \
+                 pexpect sphinxcontrib-bibtex
+
+Nix users should get the correct development environment to build the
+HTML documentation from Coq's [`default.nix`](../default.nix) (note this
+doesn't include the LaTeX packages needed to build the full documentation).
+
+### Other formats
+
+To produce the documentation in PDF and PostScript formats, the following
+additional tools are required:
+
+  - latex (latex2e)
+  - pdflatex
+  - dvips
+  - makeindex
+  - xelatex
+  - latexmk
+  - xindy
+
+All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
+install them with:
+
+    apt install texlive-full
+
+Or if you want to use less disk space:
+
+    apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
+                latexmk xindy
+
+Compilation
+-----------
+
+To produce all documentation about Coq in all formats, just run:
+
+    ./configure           # (if you hadn't already)
+    make doc
+
+
+Alternatively, you can use some specific targets:
+
+- `make doc-ps`
+  to produce all PostScript documents
+
+- `make doc-pdf`
+  to produce all PDF documents
+
+- `make doc-html`
+  to produce all HTML documents
+
+- `make refman`
+  to produce the HTML and PDF versions of the reference manual
+
+- `make refman-{html,pdf}`
+  to produce only one format of the reference manual
+
+- `make stdlib`
+  to produce all formats of the Coq standard library
+
+
+Also note the `-with-doc yes` option of `./configure` to enable the
+build of the documentation as part of the default make target.
+
+If you're editing Sphinx documentation, set SPHINXWARNERROR to 0
+to avoid treating Sphinx warnings as errors.  Otherwise, Sphinx quits
+upon detecting the first warning.  You can set this on the Sphinx `make`
+command line or as an environment variable:
+
+- `make refman SPHINXWARNERROR=0`
+
+- ~~~
+  export SPHINXWARNERROR=0
+    ⋮
+  make refman
+  ~~~
+
+Installation
+------------
+
+To install all produced documents, do:
+
+    make install-doc
+
+This will install the documentation in `/usr/share/doc/coq` unless you
+specify another value through the `-docdir` option of `./configure` or the
+`DOCDIR` environment variable.
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 8b137891..b58148ff 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -1 +1,77 @@
-
+plugins/btauto/Algebra.v
+plugins/btauto/Btauto.v
+plugins/btauto/Reflect.v
+plugins/derive/Derive.v
+plugins/extraction/ExtrHaskellBasic.v
+plugins/extraction/ExtrHaskellNatInt.v
+plugins/extraction/ExtrHaskellNatInteger.v
+plugins/extraction/ExtrHaskellNatNum.v
+plugins/extraction/ExtrHaskellString.v
+plugins/extraction/ExtrHaskellZInt.v
+plugins/extraction/ExtrHaskellZInteger.v
+plugins/extraction/ExtrHaskellZNum.v
+plugins/extraction/ExtrOcamlBasic.v
+plugins/extraction/ExtrOcamlBigIntConv.v
+plugins/extraction/ExtrOcamlIntConv.v
+plugins/extraction/ExtrOcamlNatBigInt.v
+plugins/extraction/ExtrOcamlNatInt.v
+plugins/extraction/ExtrOcamlString.v
+plugins/extraction/ExtrOcamlZBigInt.v
+plugins/extraction/ExtrOcamlZInt.v
+plugins/extraction/Extraction.v
+plugins/funind/FunInd.v
+plugins/funind/Recdef.v
+plugins/ltac/Ltac.v
+plugins/micromega/Env.v
+plugins/micromega/EnvRing.v
+plugins/micromega/Fourier.v
+plugins/micromega/Fourier_util.v
+plugins/micromega/Lia.v
+plugins/micromega/Lqa.v
+plugins/micromega/Lra.v
+plugins/micromega/MExtraction.v
+plugins/micromega/OrderedRing.v
+plugins/micromega/Psatz.v
+plugins/micromega/QMicromega.v
+plugins/micromega/RMicromega.v
+plugins/micromega/Refl.v
+plugins/micromega/RingMicromega.v
+plugins/micromega/Tauto.v
+plugins/micromega/VarMap.v
+plugins/micromega/ZCoeff.v
+plugins/micromega/ZMicromega.v
+plugins/nsatz/Nsatz.v
+plugins/omega/Omega.v
+plugins/omega/OmegaLemmas.v
+plugins/omega/OmegaPlugin.v
+plugins/omega/OmegaTactic.v
+plugins/omega/PreOmega.v
+plugins/quote/Quote.v
+plugins/romega/ROmega.v
+plugins/romega/ReflOmegaCore.v
+plugins/rtauto/Bintree.v
+plugins/rtauto/Rtauto.v
+plugins/setoid_ring/Algebra_syntax.v
+plugins/setoid_ring/ArithRing.v
+plugins/setoid_ring/BinList.v
+plugins/setoid_ring/Cring.v
+plugins/setoid_ring/Field.v
+plugins/setoid_ring/Field_tac.v
+plugins/setoid_ring/Field_theory.v
+plugins/setoid_ring/InitialRing.v
+plugins/setoid_ring/Integral_domain.v
+plugins/setoid_ring/NArithRing.v
+plugins/setoid_ring/Ncring.v
+plugins/setoid_ring/Ncring_initial.v
+plugins/setoid_ring/Ncring_polynom.v
+plugins/setoid_ring/Ncring_tac.v
+plugins/setoid_ring/RealField.v
+plugins/setoid_ring/Ring.v
+plugins/setoid_ring/Ring_base.v
+plugins/setoid_ring/Ring_polynom.v
+plugins/setoid_ring/Ring_tac.v
+plugins/setoid_ring/Ring_theory.v
+plugins/setoid_ring/Rings_Q.v
+plugins/setoid_ring/Rings_R.v
+plugins/setoid_ring/Rings_Z.v
+plugins/setoid_ring/ZArithRing.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8c09b23a..e502cb1b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/AltBinNotations.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v
@@ -498,6 +499,9 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
+    theories/Strings/BinaryString.v
+    theories/Strings/HexString.v
+    theories/Strings/OctalString.v
   </dd>
 
   <dt> <b>Reals</b>:
@@ -583,6 +587,17 @@ through the <tt>Require Import</tt> command.</p>
     theories/Program/Combinators.v
   </dd>
 
+  <dt> <b>SSReflect</b>:
+    Base libraries for the SSReflect proof language and the
+    small scale reflection formalization technique
+  </dt>
+  <dd>
+    plugins/ssrmatching/ssrmatching.v
+    plugins/ssr/ssreflect.v
+    plugins/ssr/ssrbool.v
+    plugins/ssr/ssrfun.v
+  </dd>
+
   <dt> <b>Unicode</b>:
     Unicode-based notations
   </dt>
@@ -596,8 +611,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq86.v
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
+    theories/Compat/Coq89.v
   </dd>
 </dl>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 43802efa..bea6f240 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -8,35 +8,32 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 echo -n "Building file index-list.prehtml... "
 
-#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
-LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"`
+LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
-    i=theories/$k
-    d=`basename $i`
-      ls $i | grep -q \.v'$'
+    d=`basename $k`
+      ls $k | grep -q \.v'$'
       if [ $? = 0 ]; then
-	for j in $i/*.v; do
+	for j in $k/*.v; do
 	    b=`basename $j .v`
 	    rm -f tmp2
-	    grep -q theories/$k/$b.v tmp
+	    grep -q $k/$b.v tmp
 	    a=$?
-	    grep -q theories/$k/$b.v $HIDDEN
+	    grep -q $k/$b.v $HIDDEN
 	    h=$?
 	    if [ $a = 0 ]; then
 	        if [ $h = 0 ]; then
-                    echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1
+                    echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1
                 else
-		    p=`echo $k | sed 's:/:.:g'`
-		    sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'`
+		    sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
 		    mv -f tmp2 tmp
                 fi
 	    else
 	        if [ $h = 0 ]; then
-		    echo Error: theories/$k/$b.v is missing in the template file
-                    exit 1
+		    echo Warning: $k/$b.v will be hidden from the index
                 else
-                    echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v
+                    echo Error: none of $FILE and $HIDDEN mention $k/$b.v
                     exit 1
 	        fi
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index edf4e6ec..2c69dcfe 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -560,6 +560,9 @@ class CoqtopDirective(Directive):
           Print nat.
           Definition a := 1.
 
+    The blank line after the directive is required.  If you begin a proof,
+    include an ``Abort`` afterwards to reset coqtop for the next example.
+
     Here is a list of permissible options:
 
     - Display options
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index aeadce4c..3ff00eaa 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,10 +41,13 @@ class CoqTop:
                            the ansicolors module)
         :param args:       Additional arugments to coqtop.
         """
+        BOOT = True
+        if os.getenv('COQBOOT') == "no":
+            BOOT = False
         self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
         if not pexpect.utils.which(self.coqtop_bin):
             raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
-        self.args = (args or []) + ["-boot", "-color", "on"] * color
+        self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color
         self.coqtop = None
 
     def __enter__(self):