aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.mli
diff options
context:
space:
mode:
authorEnrico Tassi2019-06-17 13:37:51 +0200
committerEnrico Tassi2019-06-17 13:37:51 +0200
commit535d897ed25f37d454b119a3873a2ff232d3f46e (patch)
treef45dbc062d15ef3637629ff7e8c17fdb73dc0289 /pretyping/pretype_errors.mli
parent658db3a8b75a338df6b07d0f0e5034bb81bcfd16 (diff)
parent135b56936e36eff23eb580c097045d2a932a19f8 (diff)
Merge PR #10332: test suite: don't try to coqchk failed tests
Reviewed-by: maximedenes
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions