Adalloc « custom « test « extraction « contrib - coq - The formal proof system

about summary refs log tree commit diff

path: root/contrib/extraction/test/custom/Adalloc

blob: 11cabe4f453406ea880298dd88c32cf5c2f1fb51 (plain)

Require Addr.
Extraction NoInline ad_double ad_double_plus_un.
Require Map.
Extraction Inline Map_rec Map_rect.