From fc0c2e19e763a4d3b4cbdb490950e0f85558e5c9 Mon Sep 17 00:00:00 2001
From: Arthur Azevedo de Amorim
Date: Tue, 22 Oct 2019 09:47:01 -0400
Subject: Add a notation for the empty type.

---
 plugins/ssr/ssrfun.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index dc774e811e..b8affba541 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -56,6 +56,10 @@ Require Import ssreflect.
                     Structure inference, as in the implementation of
                     the mxdirect predicate in matrix.v.
 
+ - The empty type:
+            void == a notation for the Empty_set type of the standard library.
+       of_void T == the canonical injection void -> T.
+
  - Sigma types:
            tag w == the i of w : {i : I & T i}.
         tagged w == the T i component of w : {i : I & T i}.
@@ -483,6 +487,12 @@ Arguments idfun {T} x /.
 
 Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
 
+(** The empty type. **)
+
+Notation void := Empty_set.
+
+Definition of_void T (x : void) : T := match x with end.
+
 (**  Strong sigma types.  **)
 
 Section Tag.
@@ -642,6 +652,9 @@ End Injections.
 Lemma Some_inj {T : nonPropType} : injective (@Some T).
 Proof. by move=> x y []. Qed.
 
+Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
+Proof. by case. Qed.
+
 (**  cancellation lemmas for dependent type casts. **)
 Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
 Proof. by case: y /. Qed.
-- 
cgit v1.2.3


From a6dc83e867c9f265076d2697d9ac8834390aa2fa Mon Sep 17 00:00:00 2001
From: Arthur Azevedo de Amorim
Date: Tue, 22 Oct 2019 10:02:11 -0400
Subject: Update changelog.

---
 doc/changelog/06-ssreflect/10932-void-type-ssr.rst | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 doc/changelog/06-ssreflect/10932-void-type-ssr.rst

diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
new file mode 100644
index 0000000000..12ac742156
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
@@ -0,0 +1,3 @@
+- Add a `void` notation for the standard library empty type (`Empty_set`)
+  (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de
+  Amorim).
-- 
cgit v1.2.3


From b70084255c48479c061e7c0407359ceadc48e72f Mon Sep 17 00:00:00 2001
From: Arthur Azevedo de Amorim
Date: Tue, 22 Oct 2019 10:12:46 -0400
Subject: Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst

Improve changelog.

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>---
 doc/changelog/06-ssreflect/10932-void-type-ssr.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
index 12ac742156..7366ef1190 100644
--- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
+++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
@@ -1,3 +1,3 @@
-- Add a `void` notation for the standard library empty type (`Empty_set`)
+- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`)
   (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de
   Amorim).
-- 
cgit v1.2.3