aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 13:04:26 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 13:04:26 +0100
commit15bcba0cb00ef759169d2ef7c3cbc21b57f133d2 (patch)
treef7081eb5dafb97f0430f5fb1877b22275e9f9696 /proofs/proof_global.ml
parent240c8bd8c1c42b0391b99f3499df1df5e5448c0e (diff)
parent7e05dec4044ad3785edc005a8504bf20819704d4 (diff)
Merge PR #6532: Fix mli-doc issue #6531
Diffstat (limited to 'proofs/proof_global.ml')
0 files changed, 0 insertions, 0 deletions