diff options
Diffstat (limited to 'test-suite/coqdoc/bug12742.v')
| -rw-r--r-- | test-suite/coqdoc/bug12742.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/coqdoc/bug12742.v b/test-suite/coqdoc/bug12742.v new file mode 100644 index 0000000000..8ce1faff00 --- /dev/null +++ b/test-suite/coqdoc/bug12742.v @@ -0,0 +1,20 @@ + (** Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + + - _Xxxxxxxxx xxxxxxx xxxxxxx_ xxxxxxx "xxxx-xxxxxx" xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx _xxxx_ xx + _xxxxx_ (xx, xxxxxxxxx, _xxx'x xxxx: xxx xxx xx xxxx_). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + + - _Xxxxx xxxxxxxxxx_ xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. +*) |