From eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 7 Mar 2021 10:15:11 -0800
Subject: Remove the :> type cast

---
 doc/sphinx/language/core/definitions.rst | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index fcf61a5bf4..1a729ced4e 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -42,7 +42,6 @@ Type cast
    term_cast ::= @term10 : @type
    | @term10 <: @type
    | @term10 <<: @type
-   | @term10 :>
 
 The expression :n:`@term10 : @type` is a type cast expression. It enforces
 the type of :n:`@term10` to be :n:`@type`.
@@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`).
 :n:`@term10 <<: @type` specifies that compilation to OCaml will be used
 to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`).
 
-:n:`@term10 :>` casts to the support type in Program mode.
-See :ref:`syntactic_control`.
-
 .. _gallina-definitions:
 
 Top-level definitions
-- 
cgit v1.2.3