aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-07-01 04:00:11 +0200
committerEmilio Jesus Gallego Arias2019-07-11 18:19:12 +0200
commit2576fee1798b753161a730244c8d4d701e8a4641 (patch)
treee07fa6b7e015b08565fd73c9f36c4dcf8cc2cfed /plugins/funind
parentefe7108a0ae32faeb674cc5d97e6fa955a1dccd8 (diff)
[proof] Minor cleanup in proof.ml
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions