aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-13 06:46:47 -0400
committerEmilio Jesus Gallego Arias2020-03-30 19:05:36 -0400
commit76115e703751cfde99d7e86be9eea8fb32398e8a (patch)
tree921df7b0e82e8681167adecc4561876489ab53e2 /vernac/comProgramFixpoint.ml
parent07a0ec4416fae0f98c610752bc73a30a30f1bd64 (diff)
[lemmas] Cleanup in handling of mutual definitions
This is a tiny step towards making the code closer to its counterpart in `DeclareDef`.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions