aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-29 00:45:16 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-29 00:45:16 +0200
commit4c1260299b707bd27765b0ab365092046b134a69 (patch)
tree22331e8562bee137a5d2eea79c0d8e3d43cb94c1 /proofs/tacmach.ml
parentf5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff)
parent8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff)
Merge PR#512: [cleanup] Unify all calls to the error function.
Diffstat (limited to 'proofs/tacmach.ml')
0 files changed, 0 insertions, 0 deletions