aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-07-14 13:53:25 +0200
committerPierre-Marie Pédrot2019-07-14 13:53:25 +0200
commit76dfd0b95a7fd2de99f65de9fc10925d58777cd4 (patch)
tree9a80f38a78b75d21b0fdd84b0a0f54a767adc290 /plugins/funind
parent3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff)
parent2576fee1798b753161a730244c8d4d701e8a4641 (diff)
Merge PR #10496: [proof] Minor cleanup in proof.ml
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions