The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Mon, 30 Jul 2001, Klaus Weich wrote:

> Note that the ocaml-compiler (at least the native one) produces, for
> 
> (match f n1 n3 with Left -> Left | Right -> Right)
> 
> or
> 
> (f n1 n3)
> 
> the same code. I.e. this optimization is already done by the (native code) 
> ocaml-compiler.

Thanks for the information. I think I will nevertheless try to put this 
kind of optimizations in the extraction code, for two reasons: 

1) to produce readable code
2) this may enable some cascade simplifications that may not be done 
by the ocaml compiler. 

I'm strongly interested by further discussions on what optimizations user
may want on extracted code, but I will be away from my mail until the end
of August.

Pierre Letouzey