diff options
| author | Pierre-Marie Pédrot | 2017-08-01 02:01:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 02:01:09 +0200 |
| commit | 60e581f6fbcf033e134291016351492d9df7e319 (patch) | |
| tree | 60bc19f6c909adafdd0e20ae14a142bffab2520d | |
| parent | 6fdec59bbd3fc67ff3b0c48193201c1739aa7f70 (diff) | |
Fixup 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 |