aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqc.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-25 09:47:20 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-25 09:47:20 +0200
commit836e0df2ee3cec97adcadd70be218d9c57bbc313 (patch)
treefb733680cc50986cba73e86c587fbeeabb837ab1 /tools/coqc.ml
parent06a723190858da8ed3f30736f22398aa7822c959 (diff)
parent7000496b6d95b67968ea49537ef9120b764cf9f4 (diff)
Merge PR #1075: Re-enable checker error messages
Diffstat (limited to 'tools/coqc.ml')
0 files changed, 0 insertions, 0 deletions