diff options
| author | Clément Pit-Claudel | 2019-05-23 14:48:52 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-23 14:48:52 -0400 |
| commit | 5cfdc20560392c2125dbcee31cfd308d5346b428 (patch) | |
| tree | b5cfa5cf2bc2c3c8aa0195e8d27629b5cf2627c1 | |
| parent | ad6e002b2d938217edb55da027ae380a6e4eff92 (diff) | |
| parent | a9697975825e408f80b488c5a7420615568b660e (diff) | |
Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 2f9c7c2b89..5f2e911ff9 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 |