aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-22 17:48:14 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-06-14 07:27:39 +0200
commit376da97be60957b25e59afb5791fae665127b17b (patch)
tree33a57ac995bbaca4566440f305b53664c9381080 /tactics/equality.ml
parent165e3000844c1e84cc5c9d1b579a0a7dab8a3684 (diff)
Remove options deprecated since 8.4.
Diffstat (limited to 'tactics/equality.ml')
0 files changed, 0 insertions, 0 deletions