aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc
diff options
context:
space:
mode:
authorCyril Cohen2020-06-09 01:16:56 +0200
committerCyril Cohen2020-06-09 04:45:15 +0200
commit8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch)
tree805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /docs/htmldoc
parent6784363d60493b8ec154bbf1e827ec677d6b5921 (diff)
fix coq 8.12 warnings
Diffstat (limited to 'docs/htmldoc')
0 files changed, 0 insertions, 0 deletions