diff options
| author |  Anton Trunov <anton.a.trunov@gmail.com> | 2018-05-25 15:26:13 +0200 |
|---|---|---|
| committer | Anton Trunov <anton.a.trunov@gmail.com> | 2018-05-25 15:26:13 +0200 |
| commit | 1ecd8d9bfca2863a86adc833d634c3f02fdc14a8 (patch) | |
| tree | aea55009d6ea093ff68cadcf8659679605d89327 /vernac/ppvernac.ml | |
| parent | da49e86de39f8d9ed8709905e63cf442745a904f (diff) | |
Fix notation for code snippet in documentation
It failed to compile before because the type arguments were declared implicit after introducing the notation
Diffstat (limited to 'vernac/ppvernac.ml')
0 files changed, 0 insertions, 0 deletions