aboutsummaryrefslogtreecommitdiff
path: root/lean-toolchain
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-08-26 00:18:26 +0200
committerAndreas Grois <andi@grois.info>2024-08-26 00:18:26 +0200
commita9ff650577b0b9c35066875d2dce7b4a72e0cb55 (patch)
tree2f8915ebf9f627967ee6a5c961c5859237bf81e9 /lean-toolchain
parente47e4b79142bcee5bcdc4647dc71c7ce3954cf0b (diff)
Remove useless proof parameter on CompleteTree.get
Diffstat (limited to 'lean-toolchain')
0 files changed, 0 insertions, 0 deletions