The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Dear all,

I would like to trace some Coq extracted code.
Something like:
Parameter Trace : nat -> unit.

Definition f (n : nat) := let _ := Trace n in n.

Extract Constant Trace => "trace_nat ».  (* Here, I will perform side-effect 
*)
Separate Extraction f.

I have the problem that the extraction mechanism is too clever.
It removes my call to Trace under the « false » assumption that it is 
side-effect free.

Is there a way to instruct the extraction not to do that ?
For instance: Hey, this is an axiom : do not assume there is no side-effect!"

It seems that disabling optimisations is not enough i.e Unset Extraction 
Optimize.

Does anyone know about any way?

Thanks,
—
Frédéric

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail