aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-08 01:23:02 -0500
committerEmilio Jesus Gallego Arias2020-04-10 01:17:07 -0400
commitaedf2c0044b04cf141a52b1398306111b0bc4321 (patch)
treedb2577695b57145cc5f032b4d6b50ebf49a60e7f /vernac/comProgramFixpoint.ml
parent795df4b7a194b53b592ed327d2318ef5abc7d131 (diff)
[ocamlformat] Enable for funind.
As part of the proof refactoring work I am doing some modifications to `funind` and indentation of that code is driving me a bit crazy; I'd much prefer to delegate it to an automatic tool.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions