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: f94ba220bf2eb9c888e9882a6dba2f42211f7743 (plain)

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