diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index 38a56d3d6b..e2aa4cfb3b 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -126,8 +126,10 @@ statically defined, but can instead by extended dynamically. A typical example is the standard `exn` type. Pattern-matching must always include a catch-all clause. They can be extended by the following command. +``` VERNAC ::= | "Ltac2" "Type" TYPEPARAMS QUALID ":=" "[" CONSTRUCTORDEF "]" +``` ## Term Syntax |