aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/class.ml
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-05-31 08:57:47 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-07-03 15:59:31 +0000
commit8520cc7a02bedf4f4820ef198550f7cfa2a6454c (patch)
tree3bec4d740b94181a1457da6c9e5f1005e8653b72 /vernac/class.ml
parentfb9755ab4445fd86cdfc5b249b487629591d87a0 (diff)
[vernac] Concrete syntax for attributes
Diffstat (limited to 'vernac/class.ml')
0 files changed, 0 insertions, 0 deletions