aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc/deps-checksum.sh
blob: e07612b84c59809f94ad5649f3ab785153d97b15 (plain)
1
2
3
4
5
rm -f misc/deps/A/*.vo misc/deps/B/*.vo
$coqc -R misc/deps/A A misc/deps/A/A.v
$coqc -R misc/deps/B A misc/deps/B/A.v
$coqc -R misc/deps/B A misc/deps/B/B.v
$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v