aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/nanoPG.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 11:09:54 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 11:09:54 +0100
commita0383d4ce6d69b086331310b32c7262223a659e5 (patch)
treeb9629546044f42266648fadd9360a54b3fe374cb /ide/nanoPG.ml
parent1e5e934a8ce31c129368e57b61e485e6b989c3f4 (diff)
Ensure locality modifiers are properly highlighted in CoqIDE.
Diffstat (limited to 'ide/nanoPG.ml')
0 files changed, 0 insertions, 0 deletions