Require Import Plus.
Extraction NoInline plus_is_one.
Require Import Addr.
Extraction NoInline ad_double ad_double_plus_un.