The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

It seems our mails crossed in the air.

> I've tried using Extract Inlined Constant for plus and
> mult, but that just performs a global renaming of plus and mult to (+)
> and (*) respectively.

Yes, that's the meaning of Extract Inlined Constant. (+) and (*) are here
your optimized Haskell operations, we replace coq extracted ops by these
ones everywhere.

> Additionally, if I just use Extract Constant
> for plus and mult, the rhs is never used in my recursively extracted
> program; the symbol mult is still used in fact_body.

One more time, this sounds quite right. The semantic of Extract Constant
is to change the _body_ of the concerned constant, but not the call sites:

let mult = (*)

let rec fact = .... mult ....

So it's still (*) that is called at the end. In fact, using Extract Constant
or Extract Inlined Constant should lead to equivalent code, using one or
the other is rather a question of clarity, depending of the size of the
provided replacement code (a symbol like * is nicer when inlined, for
instance).

Best,
Pierre