From b0e3404de4dff81680861517f70c496af1d92bbc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 13 May 2020 19:48:08 +0200
Subject: Create a new file on Variants.

---
 doc/sphinx/language/core/variants.rst              | 24 ++++++++++++++++++++++
 .../language/gallina-specification-language.rst    | 24 ----------------------
 2 files changed, 24 insertions(+), 24 deletions(-)
 create mode 100644 doc/sphinx/language/core/variants.rst
 delete mode 100644 doc/sphinx/language/gallina-specification-language.rst

(limited to 'doc')

diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
new file mode 100644
index 0000000000..fc2481201f
--- /dev/null
+++ b/doc/sphinx/language/core/variants.rst
@@ -0,0 +1,24 @@
+Private (matching) inductive types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. attr:: private(matching)
+
+   This attribute can be used to forbid the use of the :g:`match`
+   construct on objects of this inductive type outside of the module
+   where it is defined.  There is also a legacy syntax using the
+   ``Private`` prefix (cf. :n:`@legacy_attr`).
+
+   The main use case of private (matching) inductive types is to emulate
+   quotient types / higher-order inductive types in projects such as
+   the `HoTT library <https://github.com/HoTT/HoTT>`_.
+
+.. example::
+
+   .. coqtop:: all
+
+      Module Foo.
+      #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
+      Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
+      End Foo.
+      Import Foo.
+      Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
deleted file mode 100644
index fc2481201f..0000000000
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ /dev/null
@@ -1,24 +0,0 @@
-Private (matching) inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. attr:: private(matching)
-
-   This attribute can be used to forbid the use of the :g:`match`
-   construct on objects of this inductive type outside of the module
-   where it is defined.  There is also a legacy syntax using the
-   ``Private`` prefix (cf. :n:`@legacy_attr`).
-
-   The main use case of private (matching) inductive types is to emulate
-   quotient types / higher-order inductive types in projects such as
-   the `HoTT library <https://github.com/HoTT/HoTT>`_.
-
-.. example::
-
-   .. coqtop:: all
-
-      Module Foo.
-      #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
-      Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
-      End Foo.
-      Import Foo.
-      Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
-- 
cgit v1.2.3