From 0867c1d11264b39d00f117da29cbb9d1fa1f911d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 14 May 2020 10:42:07 +0200
Subject: Add type casts to new Definitions file.

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

diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
new file mode 100644
index 0000000000..ba48ea130d
--- /dev/null
+++ b/doc/sphinx/language/core/definitions.rst
@@ -0,0 +1,24 @@
+.. index::
+   single: ... : ... (type cast)
+   single: ... <: ...
+   single: ... <<: ...
+
+Type cast
+---------
+
+.. insertprodn term_cast term_cast
+
+.. prodn::
+   term_cast ::= @term10 <: @term
+   | @term10 <<: @term
+   | @term10 : @term
+   | @term10 :>
+
+The expression :n:`@term : @type` is a type cast expression. It enforces
+the type of :n:`@term` to be :n:`@type`.
+
+:n:`@term <: @type` locally sets up the virtual machine for checking that
+:n:`@term` has type :n:`@type`.
+
+:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
+has type :n:`@type`.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
deleted file mode 100644
index ba48ea130d..0000000000
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ /dev/null
@@ -1,24 +0,0 @@
-.. index::
-   single: ... : ... (type cast)
-   single: ... <: ...
-   single: ... <<: ...
-
-Type cast
----------
-
-.. insertprodn term_cast term_cast
-
-.. prodn::
-   term_cast ::= @term10 <: @term
-   | @term10 <<: @term
-   | @term10 : @term
-   | @term10 :>
-
-The expression :n:`@term : @type` is a type cast expression. It enforces
-the type of :n:`@term` to be :n:`@type`.
-
-:n:`@term <: @type` locally sets up the virtual machine for checking that
-:n:`@term` has type :n:`@type`.
-
-:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
-has type :n:`@type`.
-- 
cgit v1.2.3