aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-05-25 15:26:13 +0200
committerGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-05-25 15:26:13 +0200
commit1ecd8d9bfca2863a86adc833d634c3f02fdc14a8 (patch)
treeaea55009d6ea093ff68cadcf8659679605d89327 /vernac
parentda49e86de39f8d9ed8709905e63cf442745a904f (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')
0 files changed, 0 insertions, 0 deletions