From a9697975825e408f80b488c5a7420615568b660e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 22 May 2019 16:54:41 +0200
Subject: Ltac2 doc fix: syntax for extending an open variant type.

---
 doc/sphinx/proof-engine/ltac2.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 1386adcd59..73eb8a7f38 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -154,7 +154,7 @@ One can define new types by the following commands.
    Records are product types with named fields and eliminated by projection.
    Likewise they can be recursive if the `rec` flag is set.
 
-   .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid := [ @ltac2_constructordef ]
+   .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid ::= [ @ltac2_constructordef ]
 
       Open variants are a special kind of variant types whose constructors are not
       statically defined, but can instead be extended dynamically. A typical example
-- 
cgit v1.2.3