aboutsummaryrefslogtreecommitdiff
path: root/doc/dir
diff options
context:
space:
mode:
authorHendrik Tews2021-01-01 22:56:48 +0100
committerhendriktews2021-01-10 20:59:43 +0100
commit0d731606bee81b2d73895a23b69e84796ea7e4e7 (patch)
tree2df103ffc973c9728a866d27ab3ea325f178658e /doc/dir
parent2d94aa0aabf0aa7087f8833e1c61d95a034e2d13 (diff)
add Coq compile test for a delayed require
Diffstat (limited to 'doc/dir')
0 files changed, 0 insertions, 0 deletions