The Coq mailing list

[Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr>]

Hi Alexandre

> But the extraction removes this call

As far as I know, no option controls this optimisation performed by 
extraction.

I ended up by passing a value the rest of the code depends on, and making the 
external function behave like the identity on that argument (and having an 
axiom about this fact).  Something like:

Parameter dump_fundef : 
  fundef -> fundef.

instead of fundef -> unit, and

Definition rtl_dump (b: bool) (i:ident) (fd:fundef) : fundef :=
    dump_fundef fd

A bit disgusting, but at least extraction stops removing the calls to 
rtl_dump.  Maybe somebody has a better workaround.

Best
-francesco