extraction vers scheme

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 406 insertions, 171 deletions

diff --git a/.depend b/.depend
index 768033f63e..cc0261d401 100644
--- a/.depend
+++ b/.depend
@@ -25,9 +25,6 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi library/nametab.cmi \
@@ -48,6 +45,9 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
 library/summary.cmi: kernel/names.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
     kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/tacexpr.cmo \
     lib/util.cmi 
@@ -64,12 +64,12 @@ parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     kernel/names.cmi lib/pp.cmi toplevel/vernacexpr.cmo 
 parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi library/nametab.cmi \
     lib/pp.cmi 
-parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/term.cmi 
-parsing/g_zsyntax.cmi: parsing/coqast.cmi 
 parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
     kernel/term.cmi lib/util.cmi 
+parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi 
+parsing/g_zsyntax.cmi: parsing/coqast.cmi 
 parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -196,7 +196,7 @@ tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
 tactics/extraargs.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
     proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi 
 tactics/extratactics.cmi: parsing/genarg.cmi kernel/names.cmi \
-    proofs/proof_type.cmi kernel/term.cmi 
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/term.cmi 
 tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
@@ -256,19 +256,19 @@ toplevel/recordobj.cmi: library/nametab.cmi proofs/proof_type.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi library/nametab.cmi kernel/term.cmi \
     lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernacexpr.cmo 
 contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
     contrib/correctness/ptype.cmi kernel/term.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -323,6 +323,8 @@ contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
 contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi contrib/extraction/table.cmi \
     kernel/term.cmi 
+contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi 
 contrib/extraction/table.cmi: kernel/names.cmi library/nametab.cmi \
     lib/util.cmi toplevel/vernacinterp.cmi 
 contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
@@ -467,34 +469,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
     kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
@@ -571,6 +563,22 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
+parsing/argextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
+    parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo 
+parsing/argextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
+    parsing/q_coqast.cmx parsing/q_util.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     proofs/tacexpr.cmo lib/util.cmi parsing/ast.cmi 
@@ -637,6 +645,12 @@ parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \
     parsing/pcoq.cmx 
+parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
+    parsing/genarg.cmi 
+parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
+    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
+    parsing/genarg.cmi 
 parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -691,12 +705,6 @@ parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
 parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
     parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/util.cmx parsing/g_zsyntax.cmi 
-parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
-    parsing/genarg.cmi 
-parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
-    parsing/genarg.cmi 
 parsing/lexer.cmo: parsing/lexer.cmi 
 parsing/lexer.cmx: parsing/lexer.cmi 
 parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
@@ -1263,16 +1271,18 @@ tactics/eqdecide.cmo: tactics/auto.cmi toplevel/cerrors.cmi \
     library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
     library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \
     parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi proofs/refiner.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+    proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
 tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx \
     parsing/coqlib.cmx kernel/declarations.cmx parsing/egrammar.cmx \
     tactics/equality.cmx tactics/extratactics.cmx parsing/genarg.cmx \
     library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
     library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \
     parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx proofs/refiner.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+    proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx 
 tactics/equality.cmo: proofs/clenv.cmi parsing/coqast.cmi parsing/coqlib.cmi \
     kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evarutil.cmi lib/gmapl.cmi tactics/hipattern.cmi \
@@ -1299,12 +1309,14 @@ tactics/equality.cmx: proofs/clenv.cmx parsing/coqast.cmx parsing/coqlib.cmx \
     kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \
     tactics/equality.cmi 
-tactics/extraargs.cmo: parsing/genarg.cmi toplevel/metasyntax.cmi \
-    parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi parsing/pptactic.cmi \
-    parsing/printer.cmi tactics/tacinterp.cmi tactics/extraargs.cmi 
-tactics/extraargs.cmx: parsing/genarg.cmx toplevel/metasyntax.cmx \
-    parsing/pcoq.cmx lib/pp.cmx parsing/ppconstr.cmx parsing/pptactic.cmx \
-    parsing/printer.cmx tactics/tacinterp.cmx tactics/extraargs.cmi 
+tactics/extraargs.cmo: parsing/extend.cmi parsing/genarg.cmi \
+    toplevel/metasyntax.cmi parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi \
+    parsing/pptactic.cmi parsing/printer.cmi tactics/tacinterp.cmi \
+    tactics/extraargs.cmi 
+tactics/extraargs.cmx: parsing/extend.cmx parsing/genarg.cmx \
+    toplevel/metasyntax.cmx parsing/pcoq.cmx lib/pp.cmx parsing/ppconstr.cmx \
+    parsing/pptactic.cmx parsing/printer.cmx tactics/tacinterp.cmx \
+    tactics/extraargs.cmi 
 tactics/extratactics.cmo: parsing/astterm.cmi tactics/autorewrite.cmi \
     toplevel/cerrors.cmi tactics/contradiction.cmi parsing/coqast.cmi \
     parsing/egrammar.cmi tactics/equality.cmi pretyping/evd.cmi \
@@ -1517,12 +1529,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
     kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1707,16 +1719,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
-    library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
-    parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \
-    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
-    library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
-    parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \
-    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     tactics/auto.cmi toplevel/class.cmi pretyping/classops.cmi \
     toplevel/command.cmi parsing/coqast.cmi library/declare.cmi \
@@ -1769,6 +1771,28 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     parsing/extend.cmx toplevel/himsg.cmx kernel/names.cmx lib/options.cmx \
     lib/pp.cmx proofs/proof_type.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+    library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
+    pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+    library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
+    pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
     library/declare.cmi pretyping/detyping.cmi library/global.cmi \
     kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \
@@ -1783,18 +1807,6 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
     pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2018,15 +2030,17 @@ contrib/extraction/common.cmo: library/declare.cmi \
     contrib/extraction/haskell.cmi contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi contrib/extraction/ocaml.cmi lib/pp.cmi \
-    lib/pp_control.cmi parsing/printer.cmi contrib/extraction/table.cmi \
-    pretyping/termops.cmi lib/util.cmi contrib/extraction/common.cmi 
+    lib/pp_control.cmi parsing/printer.cmi contrib/extraction/scheme.cmi \
+    contrib/extraction/table.cmi pretyping/termops.cmi lib/util.cmi \
+    contrib/extraction/common.cmi 
 contrib/extraction/common.cmx: library/declare.cmx \
     contrib/extraction/extraction.cmx library/global.cmx \
     contrib/extraction/haskell.cmx contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx contrib/extraction/ocaml.cmx lib/pp.cmx \
-    lib/pp_control.cmx parsing/printer.cmx contrib/extraction/table.cmx \
-    pretyping/termops.cmx lib/util.cmx contrib/extraction/common.cmi 
+    lib/pp_control.cmx parsing/printer.cmx contrib/extraction/scheme.cmx \
+    contrib/extraction/table.cmx pretyping/termops.cmx lib/util.cmx \
+    contrib/extraction/common.cmi 
 contrib/extraction/extract_env.cmo: parsing/astterm.cmi \
     contrib/extraction/common.cmi library/declare.cmi pretyping/evd.cmi \
     contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \
@@ -2060,15 +2074,15 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi 
 contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \
-    parsing/egrammar.cmi contrib/extraction/extract_env.cmi \
-    parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \
-    contrib/extraction/table.cmi tactics/tacinterp.cmi \
-    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
+    parsing/egrammar.cmi parsing/extend.cmi \
+    contrib/extraction/extract_env.cmi parsing/genarg.cmi parsing/pcoq.cmi \
+    lib/pp.cmi contrib/extraction/table.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi 
 contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \
-    parsing/egrammar.cmx contrib/extraction/extract_env.cmx \
-    parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
-    contrib/extraction/table.cmx tactics/tacinterp.cmx \
-    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
+    parsing/egrammar.cmx parsing/extend.cmx \
+    contrib/extraction/extract_env.cmx parsing/genarg.cmx parsing/pcoq.cmx \
+    lib/pp.cmx contrib/extraction/table.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx 
 contrib/extraction/haskell.cmo: contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi contrib/extraction/ocaml.cmi lib/options.cmi \
@@ -2097,6 +2111,16 @@ contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \
     library/nametab.cmx lib/options.cmx lib/pp.cmx \
     contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     contrib/extraction/ocaml.cmi 
+contrib/extraction/scheme.cmo: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi contrib/extraction/ocaml.cmi lib/options.cmi \
+    lib/pp.cmi contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
+    contrib/extraction/scheme.cmi 
+contrib/extraction/scheme.cmx: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx contrib/extraction/ocaml.cmx lib/options.cmx \
+    lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
+    contrib/extraction/scheme.cmi 
 contrib/extraction/table.cmo: kernel/declarations.cmi parsing/extend.cmi \
     library/global.cmi library/goptions.cmi library/lib.cmi \
     library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
@@ -2183,9 +2207,10 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/ctast.cmo contrib/interface/dad.cmi \
     contrib/interface/debug_tac.cmi kernel/declarations.cmi \
     library/declare.cmi parsing/egrammar.cmi kernel/environ.cmi \
-    pretyping/evd.cmi parsing/genarg.cmi library/global.cmi \
-    contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \
-    library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
+    pretyping/evd.cmi parsing/extend.cmi parsing/genarg.cmi \
+    library/global.cmi contrib/interface/history.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi \
+    toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
     contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi contrib/interface/pbp.cmi parsing/pcoq.cmi \
     proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi pretyping/pretyping.cmi \
@@ -2204,9 +2229,10 @@ contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     contrib/interface/ctast.cmx contrib/interface/dad.cmx \
     contrib/interface/debug_tac.cmx kernel/declarations.cmx \
     library/declare.cmx parsing/egrammar.cmx kernel/environ.cmx \
-    pretyping/evd.cmx parsing/genarg.cmx library/global.cmx \
-    contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
+    pretyping/evd.cmx parsing/extend.cmx parsing/genarg.cmx \
+    library/global.cmx contrib/interface/history.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx \
+    toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
     contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx contrib/interface/pbp.cmx parsing/pcoq.cmx \
     proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx pretyping/pretyping.cmx \
@@ -2311,6 +2337,14 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
     proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \
@@ -2335,14 +2369,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2513,8 +2539,6 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi library/nameops.cmi \
@@ -2539,6 +2563,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/eqdecide.cmo: parsing/grammar.cma
@@ -2599,6 +2625,8 @@ parsing/g_tactic.cmo: parsing/grammar.cma
 parsing/g_tactic.cmx: parsing/grammar.cma
 parsing/g_ltac.cmo: parsing/grammar.cma
 parsing/g_ltac.cmx: parsing/grammar.cma
+parsing/argextend.cmo: 
+parsing/argextend.cmx: 
 parsing/tacextend.cmo: 
 parsing/tacextend.cmx: 
 parsing/vernacextend.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index bbbdb186cd..fcfc52d1a6 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -28,6 +28,7 @@ parsing/g_cases.ml: parsing/grammar.cma
 parsing/g_constr.ml: parsing/grammar.cma
 parsing/g_tactic.ml: parsing/grammar.cma
 parsing/g_ltac.ml: parsing/grammar.cma
+parsing/argextend.ml: 
 parsing/tacextend.ml: 
 parsing/vernacextend.ml: 
 toplevel/mltop.ml: 
diff --git a/.depend.coq b/.depend.coq
index f057e2793f..53788ead05 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -111,7 +111,7 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
-theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo
+theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
diff --git a/Makefile b/Makefile
index 4f6463060d..acbde9f73f 100644
--- a/Makefile
+++ b/Makefile
@@ -249,6 +249,7 @@ EXTRACTIONCMO=contrib/extraction/table.cmo\
 	      contrib/extraction/mlutil.cmo\
 	      contrib/extraction/ocaml.cmo \
 	      contrib/extraction/haskell.cmo \
+              contrib/extraction/scheme.cmo \
 	      contrib/extraction/extraction.cmo \
               contrib/extraction/common.cmo \
 	      contrib/extraction/extract_env.cmo \
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b6eae0a1da..149db49540 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -187,8 +187,11 @@ module OcamlModularPp = Ocaml.Make(ModularParams)
 module HaskellMonoPp = Haskell.Make(MonoParams)
 module HaskellModularPp = Haskell.Make(ModularParams)
 
+module SchemeMonoPp = Scheme.Make(MonoParams)
+
 let pp_comment s = match lang () with 
   | Haskell -> str "-- " ++ s ++ fnl () 
+  | Scheme -> str ";" ++ s ++ fnl () 
   | Ocaml | Toplevel -> str "(* " ++ s ++ str " *)" ++ fnl ()
 
 let pp_logical_ind r = 
@@ -204,6 +207,9 @@ let set_globals () = match lang () with
   | Haskell -> 
       keywords := Haskell.keywords;
       global_ids := Haskell.keywords
+  | Scheme -> 
+      keywords := Scheme.keywords;
+      global_ids := Scheme.keywords
   | _ -> ()
 
 (*s Extraction to a file. *)
@@ -213,6 +219,7 @@ let extract_to_file f prm decls =
   let preamble = match lang () with 
     | Ocaml -> Ocaml.preamble    
     | Haskell -> Haskell.preamble
+    | Scheme -> Scheme.preamble
     | _ -> assert false 
   in 
   let pp_decl = match lang (),prm.modular with 
@@ -220,6 +227,7 @@ let extract_to_file f prm decls =
     | Ocaml, _ -> OcamlModularPp.pp_decl
     | Haskell, false -> HaskellMonoPp.pp_decl    
     | Haskell, _ -> HaskellModularPp.pp_decl
+    | Scheme, _ -> SchemeMonoPp.pp_decl
     | _ -> assert false 
   in
   let used_modules = if prm.modular then 
@@ -227,7 +235,7 @@ let extract_to_file f prm decls =
   else Idset.empty
   in 
   let print_dummy = match lang() with 
-    | Ocaml -> decl_search MLdummy' decls
+    | Ocaml | Scheme -> decl_search MLdummy' decls
     | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls)
     | _ -> assert false 
   in 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 0076b99e05..6f825c9b25 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -17,6 +17,7 @@ open Nametab
 module ToplevelPp : Mlpp
 module OcamlMonoPp : Mlpp
 module HaskellMonoPp : Mlpp
+module SchemeMonoPp:Mlpp
 
 val is_long_module : dir_path -> global_reference -> bool
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index db2e7d4f93..cf595e8df6 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -212,35 +212,37 @@ let decl_in_r r0 = function
 let pp_decl d = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_decl d
   | Haskell -> HaskellMonoPp.pp_decl d
+  | Scheme -> SchemeMonoPp.pp_decl d
   | Toplevel -> ToplevelPp.pp_decl d
 
 let pp_ast a = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_ast a
   | Haskell -> HaskellMonoPp.pp_ast a
+  | Scheme -> SchemeMonoPp.pp_ast a
   | Toplevel -> ToplevelPp.pp_ast a
 
 let pp_type t = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_type t
   | Haskell -> HaskellMonoPp.pp_type t
+  | Scheme -> SchemeMonoPp.pp_type t
   | Toplevel -> ToplevelPp.pp_type t
 
 let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
+  else if decl_is_logical_ind r then 
+    msgnl (pp_logical_ind r) 
+  else if decl_is_singleton r then 
+    msgnl (pp_singleton_ind r) 
   else
-    if decl_is_logical_ind r then 
-      msgnl (pp_logical_ind r) 
-    else if decl_is_singleton r then 
-      msgnl (pp_singleton_ind r) 
-    else
-      let prm = 
-	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
-      let decls = optimize prm (decl_of_refs [r]) in 
-      let d = list_last decls in
-      let d = if (decl_in_r r d) then d 
-      else List.find (decl_in_r r) decls
-      in msgnl (pp_decl d)
-
+    let prm = 
+      { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
+    let decls = optimize prm (decl_of_refs [r]) in 
+    let d = list_last decls in
+    let d = if (decl_in_r r d) then d 
+    else List.find (decl_in_r r) decls
+    in msgnl (pp_decl d)
+	 
 let extraction rawconstr =
   set_globals ();
   let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in
@@ -276,6 +278,7 @@ let extraction_rec = mono_extraction (None,id_of_string "Main")
 let lang_suffix () = match lang () with 
   | Ocaml -> ".ml"
   | Haskell -> ".hs"
+  | Scheme -> ".scm"
   | Toplevel -> assert false
 
 let filename f = 
@@ -284,14 +287,14 @@ let filename f =
     Some f,id_of_string (Filename.chop_suffix f s) 
   else Some (f^s),id_of_string f
 
-let lang_error () = 
-  errorlabstrm "extraction_language"
+let toplevel_error () = 
+  errorlabstrm "toplevel_extraction_language"
     (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." 
      ++ fnl () ++
      str "You should use Extraction Language Ocaml or Haskell before.") 
 
 let extraction_file f vl =
-  if lang () = Toplevel then lang_error () 
+  if lang () = Toplevel then toplevel_error () 
   else mono_extraction (filename f) vl
 
 (*s Extraction of a module. The vernacular command is 
@@ -308,39 +311,46 @@ let decl_in_m m = function
 let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
   | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
-  | Toplevel -> assert false
+  | _ -> assert false
 
-let extraction_module m =
-  if lang () = Toplevel then lang_error () 
-  else 
-    let dir_m = module_of_id m in 
-    let f = module_file_name m in
-    let prm = {modular=true; mod_name=m; to_appear=[]} in 
-    let rl = extract_module dir_m in 
-    let decls = optimize prm (decl_of_refs rl) in
-    let decls = add_ml_decls prm decls in 
-    check_one_module dir_m decls; 
-    let decls = List.filter (decl_in_m dir_m) decls in
-    extract_to_file (Some f) prm decls
+let scheme_error () = 
+  errorlabstrm "scheme_extraction_language"
+    (str "No Scheme modular extraction available yet." ++ fnl ())
 
+let extraction_module m =
+  match lang () with 
+    | Toplevel -> toplevel_error ()
+    | Scheme -> scheme_error ()
+    | _ -> 
+	let dir_m = module_of_id m in 
+	let f = module_file_name m in
+	let prm = {modular=true; mod_name=m; to_appear=[]} in 
+	let rl = extract_module dir_m in 
+	let decls = optimize prm (decl_of_refs rl) in
+	let decls = add_ml_decls prm decls in 
+	check_one_module dir_m decls; 
+	let decls = List.filter (decl_in_m dir_m) decls in
+	extract_to_file (Some f) prm decls
+	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
 let recursive_extraction_module m =
-  if lang () = Toplevel then lang_error () 
-  else 
-    let dir_m = module_of_id m in 
-    let modules,refs = 
-      modules_extract_env dir_m in
-    check_modules modules; 
-    let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-    let decls = optimize dummy_prm (decl_of_refs refs) in
-    let decls = add_ml_decls dummy_prm decls in
-    Dirset.iter 
-      (fun m ->
-	let short_m = snd (split_dirpath m) in
-	let f = module_file_name short_m in 
-	let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
-	let decls = List.filter (decl_in_m m) decls in
-	if decls <> [] then extract_to_file (Some f) prm decls)
-      modules
+  match lang () with 
+    | Toplevel -> toplevel_error () 
+    | Scheme -> scheme_error () 
+    | _ -> 
+	let dir_m = module_of_id m in 
+	let modules,refs = modules_extract_env dir_m in
+	check_modules modules; 
+	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+	let decls = optimize dummy_prm (decl_of_refs refs) in
+	let decls = add_ml_decls dummy_prm decls in
+	Dirset.iter 
+	  (fun m ->
+	     let short_m = snd (split_dirpath m) in
+	     let f = module_file_name short_m in 
+	     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
+	     let decls = List.filter (decl_in_m m) decls in
+	     if decls <> [] then extract_to_file (Some f) prm decls)
+	  modules
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 84f0f663b9..40f7c0fa69 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -26,6 +26,7 @@ open Extract_env
 VERNAC ARGUMENT EXTEND language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
+| [ "Scheme" ] -> [ Scheme ]
 | [ "Toplevel" ] -> [ Toplevel ]
 END
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
new file mode 100644
index 0000000000..e16e999f60
--- /dev/null
+++ b/contrib/extraction/scheme.ml
@@ -0,0 +1,182 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Production of Scheme syntax. *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Miniml
+open Table
+open Mlutil
+open Options
+open Nametab
+open Ocaml
+
+(*s Scheme renaming issues. *)
+
+let keywords =     
+  List.fold_right (fun s -> Idset.add (id_of_string s))
+    [ "define"; "let"; "lambda"; "lambdas"; "match-case"; 
+      "apply"; "car"; "cdr"; 
+      "error"; "delay"; "force"; "_"; "__"] 
+    Idset.empty
+    
+
+let preamble _ _ print_dummy = 
+  (if print_dummy then 
+     str "(define __ (lambda (_) __))" 
+     ++ fnl () ++ fnl()
+   else mt ())
+
+let paren st = str "(" ++ st ++ str ")"
+
+let pp_abst st = function 
+  | [] -> assert false
+  | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
+  | l -> paren 
+	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+
+(*s The pretty-printing functor. *)
+
+module Make = functor(P : Mlpp_param) -> struct
+
+let pp_global r env = P.pp_global r false (Some (snd env))
+let pp_global' r = P.pp_global r false None
+
+let rename_global r = P.rename_global r false 
+
+let empty_env () = [], P.globals()
+
+let rec apply st = function 
+  | [] -> st 
+  | a :: args -> apply (paren (st ++ spc () ++ a)) args 
+
+(*s Pretty-printing of expressions.  *)
+
+let rec pp_expr env args = 
+  let apply st = apply st args in 
+  function
+    | MLrel n -> 
+	let id = get_db_name n env in apply (pr_id id)
+    | MLapp (f,args') ->
+	let stl = List.map (pp_expr env []) args' in
+        pp_expr env (stl @ args) f
+    | MLlam _ as a -> 
+      	let fl,a' = collect_lams a in
+	let fl,env' = push_vars fl env in
+	pp_abst (pp_expr env' [] a') (List.rev fl)
+    | MLletin (id,a1,a2) ->
+	let i,env' = push_vars [id] env in
+	apply 
+	  (hv 0 
+	     (hov 2 
+		(paren 
+		   (str "let " ++ 
+		    paren 
+		      (paren 
+			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
+		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
+    | MLglob r -> 
+	apply (pp_global r env)
+    | MLcons (r,args') ->
+	assert (args=[]);
+	let st = 
+	  str "`" ++ 
+	  paren (pp_global r env ++ 
+		 (if args' = [] then mt () else (spc () ++ str ",")) ++
+		 prlist_with_sep 
+		   (fun () -> spc () ++ str ",") 
+		   (pp_expr env []) args')
+	in 
+	if Refset.mem r !cons_cofix then 
+	  paren (str "delay " ++ st)
+        else st 
+    | MLcase (t, pv) ->
+	let r,_,_ = pv.(0) in 
+	let e = if Refset.mem r !cons_cofix then 
+	  paren (str "force" ++ spc () ++ pp_expr env [] t)
+	else 
+	  pp_expr env [] t 	
+	in apply (v 3 (paren 
+			 (str "match-case " ++ e ++ fnl () ++ pp_pat env pv)))
+    | MLfix (i,ids,defs) ->
+	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+      	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
+    | MLexn s -> 
+	(* An [MLexn] may be applied, but I don't really care. *)
+	paren (str "absurd")
+    | MLdummy ->
+	str "`_" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy' -> 
+	str "__" (* idem *)
+    | MLcast (a,t) ->
+	pp_expr env args a
+    | MLmagic a ->
+	pp_expr env args a
+
+
+and pp_one_pat env (r,ids,t) = 
+  let pp_arg id = str "?" ++ pr_id id in 
+  let ids,env' = push_vars (List.rev ids) env in
+  let args = 
+    if ids = [] then mt () 
+    else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
+  in 
+  (pp_global r env ++ args), (pp_expr env' [] t)
+  
+and pp_pat env pv = 
+  prvect_with_sep fnl  
+    (fun x -> let s1,s2 = pp_one_pat env x in 
+     hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
+
+(*s names of the functions ([ids]) are already pushed in [env],
+    and passed here just for convenience. *)
+
+and pp_fix env j (ids,bl) args =
+    paren 
+      (str "letrec " ++
+       (v 0 (paren 
+	       (prvect_with_sep fnl
+		  (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
+	     fnl () ++
+      	     hov 2 (apply (pr_id (ids.(j))) args))))
+
+let pp_ast a = hov 0 (pp_expr (empty_env ()) [] a)
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+  | Dtype _ -> mt ()
+  | Dabbrev _ -> mt () 
+  | Dfix (rv, defs) ->
+      let ids = Array.map rename_global rv in 
+      let env = List.rev (Array.to_list ids), P.globals() in
+      prvect_with_sep 
+	fnl 
+	(fun (fi,ti) -> 
+	   hov 2 
+	     (paren (str "define " ++ pr_id fi ++ spc () ++ 
+		     (pp_expr env [] ti)) 
+	      ++ fnl ()))
+	(array_map2 (fun id b -> (id,b)) ids defs)
+  | Dglob (r, a) ->
+      hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++
+		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
+  | Dcustom (r,s) -> 
+      hov 2 (paren (str "define " ++ pp_global' r ++ spc () ++ str s) ++ fnl ())
+	
+let pp_type _ = mt () 
+
+end
+
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
new file mode 100644
index 0000000000..4a98e97694
--- /dev/null
+++ b/contrib/extraction/scheme.mli
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Some utility functions to be reused in module [Haskell]. *)
+
+open Pp
+open Miniml
+open Names
+open Nametab
+
+val keywords : Idset.t
+
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
+
+module Make : functor(P : Mlpp_param) -> Mlpp
+
+
+
+
+
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index ee7267f3f6..ff41f6528a 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -67,29 +67,9 @@ let check_constant r =
   else errorlabstrm "extract_constant"
 	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
 
-(*
-let string_of_varg = function
-  | VARG_IDENTIFIER id -> string_of_id id
-  | VARG_STRING s -> s
-  | _ -> assert false
-*)
-
-let no_such_reference q =
-  errorlabstrm "reference_of_varg" 
-    (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".")
-
-(*
-let reference_of_varg = function
-  | VARG_QUALID q -> 
-      (try Nametab.locate q with Not_found -> no_such_reference q)
-  | _ -> assert false
-
-let refs_of_vargl = List.map reference_of_varg
-*)
-
 (*s Target Language *)
 
-type lang = Ocaml | Haskell | Toplevel
+type lang = Ocaml | Haskell | Scheme | Toplevel
 
 let lang_ref = ref Ocaml
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 9fa7142ce8..6f30c1d81b 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -24,15 +24,9 @@ val optim :  unit -> bool
 
 module Refset : Set.S with type elt = global_reference
 
-(*s Auxiliary functions *) 
-		      
-val check_constant : global_reference -> global_reference
-
-(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*)
-
 (*s Target language. *)
 
-type lang = Ocaml | Haskell | Toplevel
+type lang = Ocaml | Haskell | Scheme | Toplevel
 
 val lang : unit -> lang 
 
@@ -67,3 +61,5 @@ val reset_extraction_inline : unit -> unit
 val extract_constant_inline : bool -> qualid located -> string -> unit
 
 val extract_inductive : qualid located -> string * string list -> unit
+
+