The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Sep 15, 2005 at 04:22:33PM -0700, Adam Chlipala wrote:

> For example, I would like to replace all uses of Coq's nat with uses
> of OCaml's int, relying on dynamic checks to determine when the
> representation is not precise enough and abort the execution.  I can
> think of some simple type-directed syntactic rewrite rules that
> would accomplish this, and there are a number of other basic but
> very worthwhile optimizations of this kind.

> Can anyone point me to an existing tool that performs such
> optimizations?

I don't know of a pre-made tool that would make this, but I suppose
that CamlP4 could be used to express the "syntactic rewrite rules" you
have in mind.

-- 
Lionel