From feaee688455d3fb84bc0ac2daf3b42b0864692de Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 23 Oct 2020 22:52:16 +0200
Subject: Correct doc using :>>

The cast keywords are <: and <<:, not :>/:>>

:>> stopped being a keyword in #13106
---
 doc/sphinx/language/core/basic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/language/core/basic.rst')

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 3cc3fe231a..b1f7646be0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -172,7 +172,7 @@ Other tokens
   (even when starting |Coq| with the `-noinit` command-line flag)::
 
     ! #[ % & ' ( () ) * + , - ->
-    . .( .. ... / : ::= := :> :>> ; < <+ <- <:
+    . .( .. ... / : ::= := :> ; < <+ <- <:
     <<: <= = => > >-> >= ? @ @{ [ ] _
     `( `{ { {| | }
 
-- 
cgit v1.2.3