aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2020-11-05 11:35:19 +0100
committerThéo Zimmermann2020-11-05 12:03:49 +0100
commit32e5107dc70d4b00a76523eb95b49856a85809a1 (patch)
treeef7ccf8d9b3f11db08dc1c6d9c5da59895360ab9 /kernel/nativelambda.mli
parent5af74f736d5d621e3934be17d25c69b4ed3c0edf (diff)
Remove parts of Tactics that were moved elsewhere.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions