aboutsummaryrefslogtreecommitdiff
path: root/dev/header.py
diff options
context:
space:
mode:
authorVincent Laporte2018-10-04 15:10:10 +0000
committerVincent Laporte2018-12-10 15:03:12 +0000
commit21bac03b0997cd79ddf6a8a9b31ee4d8ee63f50a (patch)
treefcc60d263f1ad6f6ecc7aaa469eb56d8ed4dff8d /dev/header.py
parent10b07a187522b74bbcc9355d3ff9c4153f300706 (diff)
[test-suite] Run `coqchk` on most test cases
Diffstat (limited to 'dev/header.py')
0 files changed, 0 insertions, 0 deletions