aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 18:36:09 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 18:43:03 +0200
commite699313c7a3829016c853b2a1541c2e9151d709c (patch)
tree107f752561421e85cd91e23977f3185e2dea1426 /interp/coqlib.ml
parent4abb41d008fc754f21916dcac9cce49f2d04dd6d (diff)
[toplevel] Remove unused parameter from `Vernac.process_expr`.
Diffstat (limited to 'interp/coqlib.ml')
0 files changed, 0 insertions, 0 deletions