aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/sorts.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-20 01:28:08 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-25 11:05:51 +0100
commit223db63e09d3f4b0e779961918b1fedd5cda511d (patch)
tree89325aced9131e33f1d64d3b70722e3355dd5118 /kernel/sorts.mli
parentf1c3348278fb00636e0a46595d354ffc8a00992c (diff)
Moving basic generalization tactics upwards for possible use in "intros".
Diffstat (limited to 'kernel/sorts.mli')
0 files changed, 0 insertions, 0 deletions