Require Import Addr. 
Extraction NoInline ad_double ad_double_plus_un.