aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comFixpoint.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:39:34 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:39:34 +0200
commit3d10815dd3929f718fc4ede5d5a2a1fe5ccdc351 (patch)
tree3e752cb896831a46b51c089eddb9ce3767ccc541 /vernac/comFixpoint.ml
parent39cde6238489fafd706dfe7709052df0089ab3d5 (diff)
parent5f45871feefc09f080bde2b5af349f8ccda16a84 (diff)
Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly
Diffstat (limited to 'vernac/comFixpoint.ml')
0 files changed, 0 insertions, 0 deletions