aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/syntax_def.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-19 17:07:32 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-20 15:21:27 +0100
commit1af878e0dac2198ae487d0b37438520772f28350 (patch)
tree1865cbe2a0e2a7b7485cc73f6d1c4abeb4010d63 /interp/syntax_def.mli
parent281e4cb8b04c7fd13ec6416e4dcd05ffa1f48761 (diff)
Documenting Set Bullet Behavior.
This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it.
Diffstat (limited to 'interp/syntax_def.mli')
0 files changed, 0 insertions, 0 deletions