Coq Extraction to Scheme

When using Coq extraction with Scheme as target language, the obtained files need some initial macros.

The file containing these macros:


This file is to be placed alongside the extracted file, or at least somewhere your Scheme will look into when doing a (load ...). It only includes R5RS-style macros, so it should be compatible with any decent Scheme implementation. Tested so far: bigloo, mzscheme, petite, scheme48, guile.

Nota: In the case of bigloo, you could use instead: macros_extr_bigloo.scm.
This version is much faster, since it takes advantage of bigloo's native pattern matching construct. Just rename this file into macros_extr.scm.

Nota2: In the case of guile, you should first force the support of R5RS macros via

(use-modules (ice-9 syncase))

Nota3: In the case of scheme48, you should provide an error function, even a dummy one, for instance via (define error). Moreover, it seems that you should load every file explicitely, instead of expecting your extracted file to load macros_extr.scm.

What are these macros?