aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorthery2016-07-06 13:37:34 +0200
committerthery2016-07-06 13:37:34 +0200
commit8438b97aa5c8d8464ec7389f7992520e2c176ae6 (patch)
tree83c23eb2036260be05421d28632c7e278b851ab1 /kernel/nativelambda.ml
parentabe34e282ee0a5f9cca3ea9f527b254388de2cf9 (diff)
improved complexity in nsatz
we use a hashtable to reduce the complexity of creating a duplicate-free list.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions