aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comFixpoint.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
commitb75f714c025b51ed8b4db15bfce99df2d6ae7c41 (patch)
tree4c25d6cbc0d6f62450c15ebdda03a3ada717c8e1 /vernac/comFixpoint.ml
parentb1714dcc7df330df92a935f202964a1e73e44652 (diff)
parent7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb (diff)
Merge PR #7558: [api] Make `vernac/` self-contained.
Diffstat (limited to 'vernac/comFixpoint.ml')
0 files changed, 0 insertions, 0 deletions