aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/_static/ansi-dark.css2
-rw-r--r--doc/sphinx/_static/ansi.css2
-rw-r--r--doc/sphinx/_static/coqdoc.css2
-rw-r--r--doc/sphinx/_static/notations.css2
-rw-r--r--doc/sphinx/_static/notations.js2
-rw-r--r--doc/sphinx/_static/pre-text.css2
-rw-r--r--doc/sphinx/changes.rst9
-rwxr-xr-xdoc/sphinx/conf.py5
-rw-r--r--doc/sphinx/coqdoc.css2
9 files changed, 18 insertions, 10 deletions
diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css
index a564fd70bb..bbace7c553 100644
--- a/doc/sphinx/_static/ansi-dark.css
+++ b/doc/sphinx/_static/ansi-dark.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css
index 26bd797709..b3b5341166 100644
--- a/doc/sphinx/_static/ansi.css
+++ b/doc/sphinx/_static/ansi.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css
index bbcc044a20..7a3d59d4c0 100644
--- a/doc/sphinx/_static/coqdoc.css
+++ b/doc/sphinx/_static/coqdoc.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 8322ab0137..4a5fa0b328 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js
index eb7f211e8b..63112312d0 100644
--- a/doc/sphinx/_static/notations.js
+++ b/doc/sphinx/_static/notations.js
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css
index 38d81abefe..9d133fb1aa 100644
--- a/doc/sphinx/_static/pre-text.css
+++ b/doc/sphinx/_static/pre-text.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index e5045c222a..fd84868a1f 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -609,6 +609,15 @@ Changes in 8.10+beta2
Many bug fixes and documentation improvements, in particular:
+**Tactics**
+
+- Make the :tacn:`discriminate` tactic work together with
+ :flag:`Universe Polymorphism` and equality in :g:`Type`. This,
+ in particular, makes :tacn:`discriminate` compatible with the HoTT
+ library https://github.com/HoTT/HoTT
+ (`#10205 <https://github.com/coq/coq/pull/10205>`_,
+ by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau).
+
**SSReflect**
- Make the ``case E: t`` tactic work together with
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 53309cd313..867a19efe5 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -1,8 +1,7 @@
#!/usr/bin/env python3
-# -*- coding: utf-8 -*-
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
-## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
+## v # INRIA, CNRS and contributors - Copyright 1999-2019 ##
## <O___,, # (see CREDITS file for the list of authors) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
@@ -109,7 +108,7 @@ master_doc = "index"
# General information about the project.
project = 'Coq'
-copyright = '1999-2018, Inria'
+copyright = '1999-2019, Inria, CNRS and contributors'
author = 'The Coq Development Team'
# The version info for the project you're documenting, acts as replacement for
diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css
index a34bb81ebd..2ac2af1c13 100644
--- a/doc/sphinx/coqdoc.css
+++ b/doc/sphinx/coqdoc.css
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:06:57 +0000