From 1b9de6dd87351470b53584f8b5feddf6e4d51716 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 24 Oct 2019 09:49:38 +0000
Subject: Release notes for Coq 8.10.1

---
 .../01-kernel/10904-fix-debruijn-sprop-rel.rst     |  3 --
 ...ter+fix10894-regression-ltac-uconstr-typing.rst |  1 -
 doc/sphinx/changes.rst                             | 39 ++++++++++++++++++++++
 3 files changed, 39 insertions(+), 4 deletions(-)
 delete mode 100644 doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst
 delete mode 100644 doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst

diff --git a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst b/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst
deleted file mode 100644
index 6cab6a1c13..0000000000
--- a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- Fix proof of False when using |SProp| (incorrect De Bruijn handling
-  when inferring the relevance mark of a function) (`#10904
-  <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).
diff --git a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst b/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst
deleted file mode 100644
index 9d15b7126f..0000000000
--- a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst
+++ /dev/null
@@ -1 +0,0 @@
-- Fixed bug #10894: Ltac1 regression in binding free names in uconstr (`#10899 <https://github.com/coq/coq/pull/10899>`_, by Hugo Herbelin).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index b6fcf9da22..80a24b997c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -726,6 +726,45 @@ Changes in 8.10.0
   fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
   by Vincent Laporte).
 
+Changes in 8.10.1
+~~~~~~~~~~~~~~~~~
+
+A few bug fixes and documentation improvements, in particular:
+
+**Kernel**
+
+- Fix proof of False when using |SProp| (incorrect De Bruijn handling
+  when inferring the relevance mark of a function) (`#10904
+  <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).
+
+**Tactics**
+
+- Fix an anomaly when unsolved evar in :cmd:`Add Ring`
+  (`#10891 <https://github.com/coq/coq/pull/10891>`_,
+  fixes `#9851 <https://github.com/coq/coq/issues/9851>`_,
+  by Gaëtan Gilbert).
+
+**Tactic language**
+
+- Fix Ltac regression in binding free names in uconstr
+  (`#10899 <https://github.com/coq/coq/pull/10899>`_,
+  fixes `#10894 <https://github.com/coq/coq/issues/10894>`_,
+  by Hugo Herbelin).
+
+**CoqIDE**
+
+- Fix handling of unicode input before space
+  (`#10852 <https://github.com/coq/coq/pull/10852>`_,
+  fixes `#10842 <https://github.com/coq/coq/issues/10842>`_,
+  by Arthur Charguéraud).
+
+**Extraction**
+
+- Fix custom extraction of inductives to JSON
+  (`#10897 <https://github.com/coq/coq/pull/10897>`_,
+  fixes `#4741 <https://github.com/coq/coq/issues/4741>`_,
+  by Helge Bahmann).
+
 Version 8.9
 -----------
 
-- 
cgit v1.2.3