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

---
 doc/sphinx/language/core/variants.rst              | 23 ++++++++++++++++++++++
 .../language/gallina-specification-language.rst    | 23 ----------------------
 2 files changed, 23 insertions(+), 23 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..ff4212bdd4
--- /dev/null
+++ b/doc/sphinx/language/core/variants.rst
@@ -0,0 +1,23 @@
+Variants
+~~~~~~~~
+
+.. cmd:: Variant @variant_definition {* with @variant_definition }
+
+   .. insertprodn variant_definition variant_definition
+
+   .. prodn::
+      variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations }
+
+   The :cmd:`Variant` command is similar to the :cmd:`Inductive` command, except
+   that it disallows recursive definition of types (for instance, lists cannot
+   be defined using :cmd:`Variant`). No induction scheme is generated for
+   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
+
+   This command supports the :attr:`universes(polymorphic)`,
+   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
+   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
+   :attr:`universes(noncumulative)` and :attr:`private(matching)`
+   attributes.
+
+   .. exn:: The @num th argument of @ident must be @ident in @type.
+      :undocumented:
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
deleted file mode 100644
index ff4212bdd4..0000000000
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ /dev/null
@@ -1,23 +0,0 @@
-Variants
-~~~~~~~~
-
-.. cmd:: Variant @variant_definition {* with @variant_definition }
-
-   .. insertprodn variant_definition variant_definition
-
-   .. prodn::
-      variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations }
-
-   The :cmd:`Variant` command is similar to the :cmd:`Inductive` command, except
-   that it disallows recursive definition of types (for instance, lists cannot
-   be defined using :cmd:`Variant`). No induction scheme is generated for
-   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
-
-   This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
-
-   .. exn:: The @num th argument of @ident must be @ident in @type.
-      :undocumented:
-- 
cgit v1.2.3