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

about summary refs log tree commit diff

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

blob: ad4a58735c7bca1b01d8e1250de8f54d8c2d181f (plain)

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