The Coq mailing list

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

> > Extract Constant plus => "(+)".

...

> > plus :: Prelude.Int -> Prelude.Int -> Prelude.Int
> > plus n m =
> >   (\f0 fS n -> if n <= 0 then f0 () else fS (n-1))
> >     (\_ -> m)
> >     (\p -> Prelude.succ (plus p m))
> >     n

...

> 
> So my main question is: how can I force the definitions of plus and
> mult to be the ones that I supply with the Extract Constant command, 
> producing
> Haskell code that looks like the OCaml example?
> 

Hi

This is indeed a bug. It appears to be already fixed in the trunk branch of
Coq svn, probably one of my recent commits, but the bug is still active in the
8.3 branch. I'll propagate these commits soon and make sure the bug is fixed
in the next release. Sorry for the inconvenience. As I'm not using the Haskell
extraction much myself, it might still contain some rough edges 
unfortunately...

Best

Pierre