aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-06 10:07:35 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-06 10:07:35 +0100
commitddc9728030a98b03447e321d2eb4af0d92add11f (patch)
tree6892bdb6f90ff1978824b1d2bc07f534d14d9167 /configure.ml
parent273089065edaf5d926ad820d3bc3c0dacec1b75d (diff)
parent0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 (diff)
Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions