aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-06-25 09:35:25 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-07-03 16:06:00 +0000
commit4371ff2357c11d913b163dde193255f538f3565f (patch)
tree8ea3560c5d1010729cb1f51e01eabc36a22ce36d /vernac/indschemes.ml
parent3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 (diff)
[vernac] Generic syntax for flags/attributes
Diffstat (limited to 'vernac/indschemes.ml')
0 files changed, 0 insertions, 0 deletions