From 59d0ac70a475b80d28e5d0ef4764515532d47533 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 20 May 2019 23:17:56 +0200
Subject: Minor Ltac2 documentation fix: type parameters are optional.

---
 doc/sphinx/proof-engine/ltac2.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index aa603fc966..1386adcd59 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -124,13 +124,13 @@ Type declarations
 
 One can define new types by the following commands.
 
-.. cmd:: Ltac2 Type @ltac2_typeparams @lident
+.. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident
    :name: Ltac2 Type
 
    This command defines an abstract type. It has no use for the end user and
    is dedicated to types representing data coming from the OCaml world.
 
-.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef
+.. cmdv:: Ltac2 Type {? rec} {? @ltac2_typeparams } @lident := @ltac2_typedef
 
    This command defines a type with a manifest. There are four possible
    kinds of such definitions: alias, variant, record and open variant types.
@@ -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