aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.mli
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:55:35 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:55:35 +0100
commitd531f81802c0e152e83868f467b46721e65445a9 (patch)
tree18b116c2410616e405c48011dcac146eed500f47 /tactics/elim.mli
parent5129c5b02bcab1426636d18583ec7a4a46195f0a (diff)
Remove duplicate declarations.
Diffstat (limited to 'tactics/elim.mli')
0 files changed, 0 insertions, 0 deletions