aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-08-10 11:26:30 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-08-10 11:26:30 +0200
commit90303e38d22479105927f0dd2fe95cce9447bd44 (patch)
treeab679c9f51a971c3b0f15b0b59108dbe36536fae /kernel/vconv.ml
parent8d4df809c90352035f7bc92e1f829f2d482625ed (diff)
Remove unused optional "predicative" argument.
Diffstat (limited to 'kernel/vconv.ml')
0 files changed, 0 insertions, 0 deletions