aboutsummaryrefslogtreecommitdiff
path: root/lib/pp_diff.ml
diff options
context:
space:
mode:
authorEnrico Tassi2018-12-11 17:22:17 +0100
committerEnrico Tassi2018-12-11 17:22:17 +0100
commitb96b5dc67a429bfae8ef39daa65b37e1ee5223a4 (patch)
treed004ae388ef2a05a7540d6bb1f607a62374784e1 /lib/pp_diff.ml
parentdf657bd52d20b1c41e2ef4d44bde207323de6935 (diff)
parent9cdb9e97985598bd28e31af9e4cb23ea9776626c (diff)
Merge PR #8655: Test suite: use coqc and then coqchk
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions