chamboulement du codage des indcutifs extraits; deplacements des tables; ...

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

13 files changed, 483 insertions, 595 deletions

diff --git a/.depend b/.depend
index d8deee0351..e6539d98a7 100644
--- a/.depend
+++ b/.depend
@@ -38,10 +38,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi 
 kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -61,9 +61,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/bignat.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 library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -93,6 +90,9 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/util.cmi 
 library/summary.cmi: library/libnames.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 interp/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
     lib/util.cmi 
@@ -304,20 +304,20 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
 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/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi 
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.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 
@@ -373,7 +373,8 @@ contrib/extraction/ocaml.cmi: library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi 
 contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     lib/pp.cmi 
-contrib/extraction/table.cmi: library/libnames.cmi kernel/names.cmi 
+contrib/extraction/table.cmi: library/libnames.cmi \
+    contrib/extraction/miniml.cmi kernel/names.cmi 
 contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
     proofs/tacmach.cmi 
 contrib/interface/dad.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
@@ -546,6 +547,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -554,12 +561,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -642,34 +643,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: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -772,6 +763,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.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 interp/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -1754,10 +1755,10 @@ 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/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 \
@@ -1962,14 +1963,6 @@ toplevel/toplevel.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/coqast.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
-    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \
-    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
-    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
-    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2030,6 +2023,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.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/coqast.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
+    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
+    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
 contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -2050,6 +2051,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+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: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2066,18 +2079,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.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 \
@@ -2303,20 +2304,18 @@ contrib/correctness/pwp.cmx: kernel/environ.cmx library/global.cmx \
     kernel/reduction.cmx pretyping/reductionops.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx contrib/correctness/pwp.cmi 
 contrib/extraction/common.cmo: library/declaremods.cmi \
-    contrib/extraction/extraction.cmi contrib/extraction/haskell.cmi \
-    library/lib.cmi library/libnames.cmi library/libobject.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/scheme.cmi \
+    contrib/extraction/haskell.cmi library/lib.cmi library/libnames.cmi \
+    library/libobject.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/scheme.cmi \
     contrib/extraction/table.cmi lib/util.cmi contrib/extraction/common.cmi 
 contrib/extraction/common.cmx: library/declaremods.cmx \
-    contrib/extraction/extraction.cmx contrib/extraction/haskell.cmx \
-    library/lib.cmx library/libnames.cmx library/libobject.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/scheme.cmx \
+    contrib/extraction/haskell.cmx library/lib.cmx library/libnames.cmx \
+    library/libobject.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/scheme.cmx \
     contrib/extraction/table.cmx lib/util.cmx contrib/extraction/common.cmi 
 contrib/extraction/extract_env.cmo: contrib/extraction/common.cmi \
     kernel/declarations.cmi library/declare.cmi \
@@ -2333,7 +2332,7 @@ contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \
     contrib/extraction/table.cmx lib/util.cmx \
     contrib/extraction/extract_env.cmi 
 contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
-    pretyping/evd.cmi library/global.cmi lib/gmap.cmi kernel/inductive.cmi \
+    pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \
     pretyping/inductiveops.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
@@ -2341,7 +2340,7 @@ contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
     library/summary.cmi contrib/extraction/table.cmi kernel/term.cmi \
     pretyping/termops.cmi lib/util.cmi contrib/extraction/extraction.cmi 
 contrib/extraction/extraction.cmx: kernel/declarations.cmx kernel/environ.cmx \
-    pretyping/evd.cmx library/global.cmx lib/gmap.cmx kernel/inductive.cmx \
+    pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \
     pretyping/inductiveops.cmx library/libnames.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
@@ -2358,13 +2357,15 @@ contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \
     contrib/extraction/extract_env.cmx interp/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 \
-    contrib/extraction/ocaml.cmi lib/pp.cmi lib/util.cmi \
+contrib/extraction/haskell.cmo: library/libnames.cmi \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
+    library/nameops.cmi kernel/names.cmi contrib/extraction/ocaml.cmi \
+    lib/pp.cmi parsing/printer.cmi lib/util.cmi \
     contrib/extraction/haskell.cmi 
-contrib/extraction/haskell.cmx: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
-    contrib/extraction/ocaml.cmx lib/pp.cmx lib/util.cmx \
+contrib/extraction/haskell.cmx: library/libnames.cmx \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
+    library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \
+    lib/pp.cmx parsing/printer.cmx lib/util.cmx \
     contrib/extraction/haskell.cmi 
 contrib/extraction/mlutil.cmo: library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \
@@ -2376,11 +2377,11 @@ contrib/extraction/mlutil.cmx: library/libnames.cmx \
     contrib/extraction/mlutil.cmi 
 contrib/extraction/ocaml.cmo: library/libnames.cmi \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
-    library/nameops.cmi kernel/names.cmi lib/pp.cmi \
+    library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
     contrib/extraction/table.cmi lib/util.cmi contrib/extraction/ocaml.cmi 
 contrib/extraction/ocaml.cmx: library/libnames.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
-    library/nameops.cmx kernel/names.cmx lib/pp.cmx \
+    library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
     contrib/extraction/table.cmx lib/util.cmx contrib/extraction/ocaml.cmi 
 contrib/extraction/scheme.cmo: library/libnames.cmi \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
@@ -2391,16 +2392,16 @@ contrib/extraction/scheme.cmx: library/libnames.cmx \
     library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \
     lib/pp.cmx lib/util.cmx contrib/extraction/scheme.cmi 
 contrib/extraction/table.cmo: kernel/declarations.cmi kernel/environ.cmi \
-    library/global.cmi lib/gmap.cmi library/goptions.cmi library/lib.cmi \
-    library/libnames.cmi library/libobject.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    parsing/printer.cmi kernel/reduction.cmi library/summary.cmi \
+    library/global.cmi library/goptions.cmi library/lib.cmi \
+    library/libnames.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi library/summary.cmi \
     kernel/term.cmi lib/util.cmi contrib/extraction/table.cmi 
 contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \
-    library/global.cmx lib/gmap.cmx library/goptions.cmx library/lib.cmx \
-    library/libnames.cmx library/libobject.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \
+    library/global.cmx library/goptions.cmx library/lib.cmx \
+    library/libnames.cmx library/libobject.cmx contrib/extraction/miniml.cmi \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \
     kernel/term.cmx lib/util.cmx contrib/extraction/table.cmi 
 contrib/field/field.cmo: toplevel/cerrors.cmi interp/constrintern.cmi \
     library/declare.cmi parsing/egrammar.cmi pretyping/evd.cmi \
@@ -2612,6 +2613,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx contrib/interface/ctast.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx interp/topconstr.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: proofs/clenv.cmi interp/constrintern.cmi \
     parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2636,14 +2645,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.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 \
@@ -2812,12 +2813,12 @@ 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/acic.cmo: kernel/names.cmi kernel/term.cmi 
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
     kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi 
 contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
     kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx 
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
     library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -2872,8 +2873,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
     contrib/xml/xml.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
     contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -2900,6 +2899,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/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
 tactics/tauto.cmx: parsing/grammar.cma
 tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index bfe693c64b..28f560d96b 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -19,6 +19,8 @@ open Miniml
 open Mlutil
 open Ocaml
 
+(*s Get all references used in one [ml_decl list]. *)
+
 module Orefset = struct 
   type t = { set : Refset.t ; list : global_reference list }
   let empty = { set = Refset.empty ; list = [] }
@@ -31,58 +33,12 @@ end
 
 type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
 
-let add_down o r = o.down <- Orefset.add r o.down
-let add_up o r = o.up <- Orefset.add r o.up
-let lang_add_type o r = if lang () = Haskell then add_up o r else add_down o r
-
-(*s Get all references used in one [ml_decl] list. *)
-
-let mltype_get_references o t = 
-  let rec get_rec = function 
-    | Tglob (r,l) -> lang_add_type o r; List.iter get_rec l 
-    | Tarr (a,b) -> get_rec a; get_rec b 
-    | _ -> () 
-  in get_rec t
-
-let ast_get_references o a = 
-  let rec get_rec a =
-    ast_iter get_rec a;
-    match a with 
-      | MLglob r -> add_down o r
-      | MLcons (r,_) -> add_up o r
-      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> add_up o r) v
-      | MLcast (_,t) -> mltype_get_references o t 
-      | _ -> ()
-  in get_rec a
-
-let ip_of_indref = function 
-  | IndRef ip -> ip 
-  | _ -> assert false
-
 let decl_get_references ld = 
   let o = { up = Orefset.empty ; down = Orefset.empty } in 
-  let one_decl = function 
-    | Dind (l,_) -> 
-	List.iter (fun (_,r,l) -> 
-		     lang_add_type o r; 
-		     (try 
-			List.iter (add_down o) (find_proj (ip_of_indref r))
-		      with Not_found -> ()); 
-		     List.iter (fun (r,l) -> 
-				  add_up o r; 
-				  List.iter (mltype_get_references o) l) l) l
-    | Dtype (r,_,t) -> lang_add_type o r; mltype_get_references o t 
-    | Dterm (r,a,t) -> 
-	add_down o r; ast_get_references o a; mltype_get_references o t
-    | Dfix(rv,c,t) -> 
-	Array.iter (add_down o) rv; 
-	Array.iter (ast_get_references o) c; 
-	Array.iter (mltype_get_references o) t
-    | DcustomTerm (r,_) -> add_down o r
-    | DcustomType (r,_) -> lang_add_type o r
-  in 
-  List.iter one_decl ld; 
-  o
+  let do_term r = o.down <- Orefset.add r o.down in
+  let do_cons r = o.up <- Orefset.add r o.up in 
+  let do_type = if lang () = Haskell then do_cons else do_term in 
+  List.iter (decl_iter_references do_term do_cons do_type) ld; o
 
 (*S Modules considerations. *)
 
@@ -229,17 +185,6 @@ let preamble prm = match lang () with
   | Haskell -> Haskell.preamble prm
   | Scheme -> Scheme.preamble prm
   | Toplevel -> (fun _ _ -> mt ())
-	
-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 = 
-  pp_comment (Printer.pr_global r ++ str " : logical inductive")
-
-let pp_singleton_ind r = 
-  pp_comment (Printer.pr_global r ++ str " : singleton inductive constructor")
 
 (*S Extraction to a file. *)
 
@@ -263,12 +208,6 @@ let extract_to_file f prm decls =
      decl_type_search Tdummy decls, 
      decl_type_search Tunknown decls) in 
   pp_with ft (preamble prm used_modules print_dummys);
-  if not prm.modular then begin 
-    List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
-      (List.filter Extraction.decl_is_logical_ind prm.to_appear); 
-    List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
-      (List.filter Extraction.decl_is_singleton prm.to_appear); 
-  end;
   begin try
     List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
   with e ->
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 2f420b8ad1..fb2291edfa 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -19,10 +19,6 @@ val long_module : global_reference -> dir_path
 val create_mono_renamings : ml_decl list -> unit
 val set_keywords : unit -> unit
 
-val pp_logical_ind : global_reference -> std_ppcmds
-
-val pp_singleton_ind : global_reference -> std_ppcmds
-
 val pp_decl : unit -> ml_decl -> std_ppcmds
 
 val segment_contents : Lib.library_segment -> global_reference list
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9d1808a76d..7d19fa68d7 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -179,8 +179,7 @@ let check_r m sm r =
 let check_decl m sm = function 
   | Dterm (r,_,_) -> check_r m sm r 
   | Dtype (r,_,_) -> check_r m sm r
-  | Dind ((_,r,_)::_, _) -> check_r m sm r 
-  | Dind ([],_) -> ()
+  | Dind (kn,_) -> check_r m sm (IndRef (kn,0))
   | DcustomTerm (r,_) ->  check_r m sm r
   | DcustomType (r,_) ->  check_r m sm r	
   | Dfix(rv,_,_) -> Array.iter (check_r m sm) rv 
@@ -280,13 +279,13 @@ and visit_ast m eenv a =
   in
   visit a
 
-and visit_inductive m eenv inds =
-  let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in
-  let visit_ind (_,_,cl) = List.iter visit_constructor cl in
-  List.iter visit_ind inds
+and visit_inductive m eenv ind =
+  let visit_constructor tl = List.iter (visit_type m eenv) tl in
+  let visit_packet p = Array.iter visit_constructor p.ip_types in
+  Array.iter visit_packet ind.ind_packets
 
 and visit_decl m eenv = function
-  | Dind (inds,_) -> visit_inductive m eenv inds
+  | Dind (_,ind) -> visit_inductive m eenv ind
   | Dtype (_,_,t) -> visit_type m eenv t
   | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
   | Dfix (_,c,t) -> 
@@ -333,8 +332,7 @@ let print_user_extract r =
 let decl_in_r r0 = function 
   | Dterm (r,_,_) -> r = r0
   | Dtype (r,_,_) -> r = r0
-  | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
-  | Dind ([],_) -> false
+  | Dind (kn, _) -> kn = kn_of_r r0
   | DcustomTerm (r,_) ->  r = r0 
   | DcustomType (r,_) ->  r = r0 
   | Dfix (rv,_,_) -> array_exists ((=) r0) rv
@@ -343,10 +341,6 @@ let extraction qid =
   let r = Nametab.global qid in 
   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 
     let prm = 
       { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
@@ -404,8 +398,7 @@ let extraction_file f vl =
 let decl_in_m m = function 
   | Dterm (r,_,_) -> m = long_module r
   | Dtype (r,_,_) -> m = long_module r
-  | Dind ((_,r,_)::_, _) -> m = long_module r 
-  | Dind ([],_) -> false
+  | Dind (kn,_) -> m = long_module (IndRef (kn,0))
   | DcustomTerm (r,_) ->  m = long_module r
   | DcustomType (r,_) ->  m = long_module r
   | Dfix (rv,_,_) -> m = long_module rv.(0)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 76b4133aba..6e1cdcfccb 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -29,7 +29,17 @@ open Table
 open Mlutil
 (*i*)
 
-(*S Extraction results. *)
+exception I of inductive_info
+
+let none = Evd.empty
+
+let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
+
+let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
+
+let is_axiom kn = (Global.lookup_constant kn).const_body = None
+
+(*S Generation of flags and signatures. *)
 
 (* The type [flag] gives us information about any Coq term: 
    \begin{itemize}
@@ -51,77 +61,6 @@ type scheme = TypeScheme | Default
 
 type flag = info * scheme
 
-(* The [signature] type is used to know how many arguments a CIC
-   object expects, and what these arguments will become in the ML
-   object. *)
-   
-(* Convention: outmost lambda/product gives the head of the list, 
-   and [true] means that the argument is to be kept. *)
-
-type signature = bool list
-
-(* The [ind_extraction_result] is used to save the extraction of 
-   an inductive type. In the informative case, it stores a signature 
-   and a type variable list. *)
-
-type ind_extraction_result = signature * identifier list 
-
-(* For an informative constructor, the [cons_extraction_result] 
-   contains the list of the types of its arguments and the number of 
-   parameters to discard. *)
-
-type cons_extraction_result = ml_type list * int  
-
-(*S Tables to keep the extraction results. *)
-
-let visited_inductive = ref KNset.empty
-let visit_inductive k = visited_inductive := KNset.add k !visited_inductive
-let already_visited_inductive k = KNset.mem k !visited_inductive
-
-let inductive_table = 
-  ref (Gmap.empty : (inductive, ind_extraction_result) Gmap.t)
-let add_inductive i e = inductive_table := Gmap.add i e !inductive_table
-let lookup_inductive i = Gmap.find i !inductive_table
-
-let constructor_table = 
-  ref (Gmap.empty : (constructor, cons_extraction_result) Gmap.t)
-let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
-let lookup_constructor c = Gmap.find c !constructor_table
-
-let cst_term_table = ref (KNmap.empty : ml_decl KNmap.t)
-let add_cst_term kn d = cst_term_table := KNmap.add kn d !cst_term_table
-let lookup_cst_term kn = KNmap.find kn !cst_term_table
-
-let cst_type_table = ref (KNmap.empty : ml_schema KNmap.t)
-let add_cst_type kn s = cst_type_table := KNmap.add kn s !cst_type_table
-let lookup_cst_type kn = KNmap.find kn !cst_type_table 
-
-(* Tables synchronization. *)
-
-let freeze () =
-  !visited_inductive, !inductive_table, 
-  !constructor_table, !cst_term_table, !cst_type_table
-
-let unfreeze (vi,it,ct,te,ty) =
-  visited_inductive := vi; inductive_table := it; constructor_table := ct;
-  cst_term_table := te; cst_type_table := ty
-
-let _ = declare_summary "Extraction tables"
-	  { freeze_function = freeze;
-	    unfreeze_function = unfreeze;
-	    init_function = (fun () -> ());
-	    survive_section = true }
-
-(*S Generation of flags and signatures. *)
-
-let none = Evd.empty
-
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
-
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
-
-let is_axiom kn = (Global.lookup_constant kn).const_body = None
-
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
@@ -251,8 +190,8 @@ let rec extract_type env db j c args =
 	(* There are two kinds of informative axioms here, *)
 	(* - the types that should be realized via [Extract Constant] *)
 	(* - the type schemes that are not realizable (yet). *) 
-	if args = [] then error_axiom kn
-	else error_axiom_scheme kn 
+	if args = [] then error_axiom (ConstRef kn)
+	else error_axiom_scheme (ConstRef kn) 
     | Const kn ->
 	let body = constant_value env kn in 
 	let mlt1 = extract_type env db j (applist (body, args)) [] in 
@@ -266,9 +205,9 @@ let rec extract_type env db j c args =
 		 (* reduction. Try to find the shortest correct answer. *) 
 		 if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1
 	   | None -> mlt1)
-    | Ind kni ->
-	let si = fst (extract_inductive kni) in 
-	extract_type_app env db (IndRef kni,si) args
+    | Ind ((kn,i) as ip) ->
+	let s = (extract_inductive kn).ind_packets.(i).ip_sign in  
+	extract_type_app env db (IndRef ip,s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
@@ -320,78 +259,71 @@ and extract_type_scheme env db c p =
 
 (*S Extraction of an inductive type. *)
 
-(* [extract_inductive] answers a [ind_extraction_result] in
-   case of an informative inductive, and raises [Not_found] otherwise *)
-
-and extract_inductive ((kn,_) as i) =
-  if not (already_visited_inductive kn) then extract_mib kn; 
-  lookup_inductive i
-			     
-(* [extract_constructor] answers a [cons_extraction_result] in
-   case of an informative constructor, and raises [Not_found] otherwise *)
-
-and extract_constructor (((kn,_),_) as c) =
-  if not (already_visited_inductive kn) then extract_mib kn; 
-  lookup_constructor c
-
-(* The real job: *)
-
-and extract_mib kn =
-  visit_inductive kn; 
-  add_recursors kn; 
-  let env = Global.env () in 
-  let (mib,mip) = Global.lookup_inductive (kn,0) in
-  (* Everything concerning parameters. *)
-  (* We do that first, since they are common to all the [mib]. *)
-  let params_nb = mip.mind_nparams in
-  let params_env = push_rel_context mip.mind_params_ctxt env in
-  (* First pass: we store inductive signatures together with *)
-  (* their type var list. *)
-  for i = 0 to mib.mind_ntypes - 1 do
-    let mip = snd (Global.lookup_inductive (kn,i)) in 
-    if mip.mind_sort <> (Prop Null) then 
-      let ip = (kn,i) in 
-      let s,vl = type_sign_vl env mip.mind_nf_arity in 
-      add_inductive ip (s,vl); 
-  done;
-  (* Second pass: we extract constructors *)
-  for i = 0 to mib.mind_ntypes - 1 do
-    let ip = (kn,i) in 
-    let mip = snd (Global.lookup_inductive ip) in
-    if mip.mind_sort <> (Prop Null) then
-      let s = fst (lookup_inductive ip) in 
-      let types = arities_of_constructors env ip in
-      for j = 0 to Array.length types - 1 do 
-	let t = snd (decompose_prod_n params_nb types.(j)) in
-	let args = match kind_of_term (snd (decompose_prod t)) with
-	  | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
-	  | _ -> [||]
+and extract_inductive kn =
+  try lookup_ind kn with Not_found -> 
+    add_recursors kn; 
+    let env = Global.env () in 
+    let (mib,mip) = Global.lookup_inductive (kn,0) in
+    (* Everything concerning parameters. *)
+    (* We do that first, since they are common to all the [mib]. *)
+    let npar = mip.mind_nparams in
+    let epar = push_rel_context mip.mind_params_ctxt env in
+    (* First pass: we store inductive signatures together with *)
+    (* their type var list. *)
+    let packets = 
+      Array.map 
+	(fun mip -> 
+	   let b = mip.mind_sort <> (Prop Null) in 
+	   let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in
+	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
+	   { ip_logical = (not b); ip_sign = s; ip_vars = v; ip_types = t }) 
+	mib.mind_packets 
+    in 
+    add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets};
+    (* Second pass: we extract constructors *)
+    for i = 0 to mib.mind_ntypes - 1 do
+      let p = packets.(i) in 
+      if not p.ip_logical then
+	let types = arities_of_constructors env (kn,i) in 
+	for j = 0 to Array.length types - 1 do 
+	  let t = snd (decompose_prod_n npar types.(j)) in
+	  let args = match kind_of_term (snd (decompose_prod t)) with
+	    | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+	    | _ -> [||]
+	  in 
+	  let dbmap = parse_ind_args p.ip_sign args (nb_prod t + npar) in 
+	  let db = db_from_ind dbmap npar in 
+	  p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
+	done
+    done;
+    (* Third pass: we determine special cases. *)
+    let ind_info = 
+      try 
+	if not mib.mind_finite then raise (I Coinductive); 
+	if mib.mind_ntypes <> 1 then raise (I Standard); 
+	let p = packets.(0) in 
+	if p.ip_logical then raise (I Standard);
+	if Array.length p.ip_types <> 1 then raise (I Standard);
+	let typ = p.ip_types.(0) in 
+	let l = List.filter (type_neq mlt_env Tdummy) typ in 
+	if List.length l = 1 && not (type_mem_kn kn (List.hd l)) 
+	then raise (I Singleton); 
+	if l = [] then raise (I Standard); 
+	let projs = 
+	  try (find_structure (kn,0)).s_PROJ 
+	  with Not_found -> raise (I Standard);
 	in 
-	let dbmap = parse_ind_args s args (nb_prod t + params_nb) in 
-	let db = db_from_ind dbmap params_nb in 
-	let l = extract_type_cons params_env db dbmap t (params_nb+1) in 
-	add_constructor (ip,j+1) (l,params_nb)
-      done
-  done;
-  (* Record tables: *)
-  if mib.mind_ntypes = 1 then 
-    let ip = (kn,0) in 
-    let mip = snd (Global.lookup_inductive ip) in
-    if (mip.mind_sort <> (Prop Null))
-      && (Array.length mip.mind_consnames = 1)
-      && not (is_singleton_inductive ip) 
-    then try
-      let typs = fst (lookup_constructor (ip,1)) in 
-      let s = List.map (type_neq mlt_env Tdummy) typs in
-      if not (List.mem true s) then raise Not_found; 
-      let projs = (find_structure ip).s_PROJ in 
-      assert (List.length s = List.length projs); 
-      let check (_,o) = match o with 
-	| None -> raise Not_found 
-	| Some kn -> ConstRef kn 
-      in 
-      add_record ip (List.map check (List.filter fst (List.combine s projs)))
-    with Not_found  -> () 
+	let s = List.map (type_neq mlt_env Tdummy) l in
+	let check (_,o) = match o with 
+	  | None -> raise (I Standard)
+	  | Some kn -> ConstRef kn 
+	in  
+	add_record kn (List.map check (List.filter fst (List.combine s projs))); 
+	raise (I Record)
+      with (I info) -> info
+    in
+    let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in 
+    add_ind kn i; i
 
 (*s [extract_type_cons] extracts the type of an inductive 
   constructor toward the corresponding list of ML types. *)
@@ -411,29 +343,11 @@ and extract_type_cons env db dbmap c i =
 	(extract_type env db 0 t []) :: l 
     | _ -> [] 
 
-(*s Looking for informative singleton case, i.e. an inductive with one 
-   constructor which has one informative argument. This dummy case will 
-   be simplified. *)
-
-and is_singleton_inductive ip = 
-  let (mib,mip) = Global.lookup_inductive ip in 
-  mib.mind_finite &&
-  (mib.mind_ntypes = 1) &&
-  (Array.length mip.mind_consnames = 1) && 
-  try 
-    let l = 
-      List.filter (type_neq mlt_env Tdummy) (fst (extract_constructor (ip,1)))
-    in List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l))
-  with Not_found -> false
-          
-and is_singleton_constructor ((kn,i),_) = 
-  is_singleton_inductive (kn,i) 
-
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
 and mlt_env r = match r with 
   | ConstRef kn -> 
-      (try match lookup_cst_term kn with 
+      (try match lookup_term kn with 
 	 | Dtype (_,vl,mlt) -> Some mlt
 	 | _ -> None
        with Not_found -> 
@@ -449,7 +363,7 @@ and mlt_env r = match r with
 		      let s,vl = type_sign_vl env typ in 
 		      let db = db_from_sign s in 
 		      let t = extract_type_scheme env db body (List.length s) 
-		      in add_cst_term kn (Dtype (r, vl, t)); Some t
+		      in add_term kn (Dtype (r, vl, t)); Some t
 		  | _ -> None))
   | _ -> None
 
@@ -461,12 +375,12 @@ let type_expunge = type_expunge mlt_env
 (*s Extraction of the type of a constant. *)
 
 let record_constant_type kn = 
-  try lookup_cst_type kn
+  try lookup_type kn
   with Not_found -> 
     let env = Global.env () in 
     let mlt = extract_type env [] 1 (constant_type env kn) [] in 
     let schema = (type_maxvar mlt, mlt)
-    in add_cst_type kn schema; schema
+    in add_type kn schema; schema
 
 (*S Extraction of a term. *)
 
@@ -603,14 +517,16 @@ and extract_cst_app env mle mlt kn args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt ((ip,_) as cp) args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
-  let types, params_nb = extract_constructor cp in
-  let types = List.map type_expand types in
-  let nb_tvar = List.length (snd (extract_inductive ip)) in 
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in 
+  let mi = extract_inductive kn in 
+  let params_nb = mi.ind_nparams in 
+  let oi = mi.ind_packets.(i) in 
+  let nb_tvars = List.length oi.ip_vars
+  and types = List.map type_expand oi.ip_types.(j-1) in
+  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in 
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
-  let type_cons = instantiation (nb_tvar, type_cons) in 
+  let type_cons = instantiation (nb_tvars, type_cons) in 
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map ((<>) Tdummy) types in
   let ls = List.length s in 
@@ -624,7 +540,7 @@ and extract_cons_app env mle mlt ((ip,_) as cp) args =
   (* If stored and expected types differ, then magic! *)
   let magic = needs_magic (type_cons, type_head) in 
   let head mla = 
-    if is_singleton_constructor cp then 
+    if mi.ind_info = Singleton then 
       put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *)
     else put_magic_if magic (MLcons (ConstructRef cp, mla))
   in 
@@ -643,7 +559,7 @@ and extract_cons_app env mle mlt ((ip,_) as cp) args =
 
 (*S Extraction of a case. *)
 
-and extract_case env mle (ip,c,br) mlt = 
+and extract_case env mle ((kn,i) as ip,c,br) mlt = 
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
   let ni = mis_constr_nargs ip in
@@ -665,8 +581,10 @@ and extract_case env mle (ip,c,br) mlt =
 	snd (case_expunge s e)
       end 
     else 
-      let nb_tvar = List.length (snd (extract_inductive ip)) in 
-      let metas = Array.init nb_tvar new_meta in 
+      let mi = extract_inductive kn in 
+      let params_nb = mi.ind_nparams in 
+      let oi = mi.ind_packets.(i) in 
+      let metas = Array.init (List.length oi.ip_vars) new_meta in 
       (* The extraction of the head. *)
       let type_head = Tglob (IndRef ip, Array.to_list metas) in
       let a = extract_term env mle type_head c [] in 
@@ -674,14 +592,14 @@ and extract_case env mle (ip,c,br) mlt =
       let extract_branch i = 
 	(* The types of the arguments of the corresponding constructor. *)
 	let f t = type_subst_vect metas (type_expand t) in 
-	let l = List.map f (fst (extract_constructor (ip,i+1))) in
+	let l = List.map f oi.ip_types.(i) in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
 	(ConstructRef (ip,i+1), List.rev ids, e)
       in
-      if is_singleton_inductive ip then 
+      if mi.ind_info = Singleton then 
 	begin 
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
@@ -733,11 +651,11 @@ let extract_constant kn r =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if isSort typ then error_axiom kn 
-	       else error_axiom_scheme kn
-           | (Info,Default) -> error_axiom kn 
-           | (Logic,TypeScheme) -> warning_axiom kn; Dtype (r, [], Tdummy)
-	   | (Logic,Default) -> warning_axiom kn; Dterm (r, MLdummy, Tdummy))
+	       if isSort typ then error_axiom r
+	       else error_axiom_scheme r
+           | (Info,Default) -> error_axiom r 
+           | (Logic,TypeScheme) -> warning_axiom r; Dtype (r, [], Tdummy)
+	   | (Logic,Default) -> warning_axiom r; Dterm (r, MLdummy, Tdummy))
     | Some l_body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
@@ -774,42 +692,18 @@ let extract_constant kn r =
                Dtype (r, vl, t))
 
 let extract_constant_cache kn r = 
-  try lookup_cst_term kn 
+  try lookup_term kn 
   with Not_found ->
     let d = extract_constant kn r
-    in add_cst_term kn d; d
-
-(*s From an inductive to a ML declaration. *)
-
-let extract_inductive_declaration kn =
-  if not (already_visited_inductive kn) then extract_mib kn; 
-  let ip = (kn,0) in 
-  if is_singleton_inductive ip then
-    let t = 
-      List.hd (List.filter (type_neq Tdummy) (fst (lookup_constructor (ip,1))))
-    and vl = snd (lookup_inductive ip) in 
-    Dtype (IndRef ip,vl,t)
-  else
-    let mib = Global.lookup_mind kn in
-    let one_ind ip n = 
-      iterate_for (-n) (-1)
-	(fun j l -> 
-	   let cp = (ip,-j) in 
-	   let mlt = fst (lookup_constructor cp) in 
-	   (ConstructRef cp, List.filter (type_neq Tdummy) mlt)::l) []
-    in
-    let l = 
-      iterate_for (1 - mib.mind_ntypes) 0
-	(fun i acc -> 
-	   let ip = (kn,-i) in
-	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
-	   try 
-	     let vl = snd (lookup_inductive ip) in 
-	     (vl, IndRef ip, one_ind ip nc) :: acc
-	   with Not_found -> acc)
-	[] 
-    in
-    Dind (l, not mib.mind_finite)
+    in add_term kn d; d
+
+let extract_inductive_declaration kn = 
+  let ind = extract_inductive kn in 
+  let f l = List.filter (type_neq Tdummy) l in 
+  let packets = 
+    Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) 
+      ind.ind_packets
+  in Dind (kn,{ ind with ind_packets = packets })
 
 (*s From a global reference to a ML declaration. *)
 
@@ -819,19 +713,4 @@ let extract_declaration r = match r with
   | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
   | VarRef kn -> error_section ()
 
-(*s Check if a global reference corresponds to a logical inductive. *)
-
-let decl_is_logical_ind = function 
-  | IndRef ip -> (try ignore (extract_inductive ip); false with _ -> true)
-  | ConstructRef cp -> 
-      (try ignore (extract_constructor cp); false with _ -> true)
-  | _ -> false
-
-(*s Check if a global reference corresponds to the constructor of 
-  a singleton inductive. *)
-
-let decl_is_singleton = function 
-  | ConstructRef cp -> is_singleton_constructor cp 
-  | _ -> false 
-
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b8e74961b8..268a68692f 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -17,12 +17,3 @@ open Miniml
 
 val extract_declaration : global_reference -> ml_decl
 
-(*s Check whether a global reference corresponds to a logical inductive. *)
-
-val decl_is_logical_ind : global_reference -> bool
-
-(*s Check if a global reference corresponds to the constructor of 
-  a singleton inductive. *)
-
-val decl_is_singleton : global_reference -> bool
-
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 149b9967cb..81ec48767a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -14,6 +14,7 @@ open Pp
 open Util
 open Names
 open Nameops
+open Libnames
 open Miniml
 open Mlutil
 open Ocaml
@@ -176,7 +177,25 @@ and pp_function env f t =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_one_inductive (pl,name,cl) =
+let pp_comment s = str "-- " ++ s ++ fnl ()
+
+let pp_logical_ind ip packet = 
+  pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+  pp_comment (str "with constructors : " ++ 
+	      prvect_with_sep spc Printer.pr_global 
+		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
+
+let pp_singleton kn packet = 
+  let l = rename_tvars keywords packet.ip_vars in 
+  let l' = List.rev l in 
+  hov 0 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ 
+	 prlist_with_sep spc pr_id l ++
+	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
+	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+		     Printer.pr_global (ConstructRef ((kn,0),1))))
+
+let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
     (pp_global r ++
@@ -186,25 +205,32 @@ let pp_one_inductive (pl,name,cl) =
       	       	prlist_with_sep 
 		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
   in
-  (str (if cl = [] then "type " else "data ") ++ 
-   pp_global name ++ str " " ++
-   prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
-   (if pl = [] then (mt ()) else (str " ")) ++
-   if cl = [] then str "= () -- empty inductive"
-   else 
-      (v 0 (str "= " ++
-	    prlist_with_sep (fun () -> (fnl () ++ str "  | "))
-              pp_constructor cl)))
+  str (if cv = [||] then "type " else "data ") ++ 
+  pp_global (IndRef ip) ++ str " " ++
+  prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
+  (if pl = [] then mt () else str " ") ++
+  if cv = [||] then str "= () -- empty inductive"
+  else 
+    (v 0 (str "= " ++
+	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor 
+	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
   
-let pp_inductive il =
-  (prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ())
+let rec pp_ind kn i ind =
+  if i >= Array.length ind.ind_packets then mt ()
+  else 
+    let ip = (kn,i) in 
+    let p = ind.ind_packets.(i) in 
+    if p.ip_logical then  
+      pp_logical_ind ip p ++ pp_ind kn (i+1) ind
+    else 
+      pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ pp_ind kn (i+1) ind
+
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dind ([], _) -> mt ()
-  | Dind (i, _) -> 
-      hov 0 (pp_inductive i)
+  | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0)
+  | Dind (kn,i) -> hov 0 (pp_ind kn 0 i)
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in
       let l' = List.rev l in 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 199bb9e0cc..6f56f36e30 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -15,6 +15,15 @@ open Util
 open Names
 open Libnames
 
+(* The [signature] type is used to know how many arguments a CIC
+   object expects, and what these arguments will become in the ML
+   object. *)
+   
+(* Convention: outmost lambda/product gives the head of the list, 
+   and [true] means that the argument is to be kept. *)
+
+type signature = bool list
+
 (*s ML type expressions. *)
 
 type ml_type = 
@@ -27,7 +36,7 @@ type ml_type =
   | Tunknown
   | Tcustom of string
 
-and ml_meta = { id : int; mutable contents : ml_type option}
+and ml_meta = { id : int; mutable contents : ml_type option }
 
 (* ML type schema. 
    The integer is the number of variable in the schema. *)
@@ -36,11 +45,28 @@ type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type ml_one_ind = 
-  identifier list * global_reference * (global_reference * ml_type list) list
+type inductive_info = Record | Singleton | Coinductive | Standard
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. 
+   If the inductive is logical ([ip_logical = false]), then all other fields
+   are unused. Otherwise, 
+   [ip_sign] is a signature concerning the arguments of the inductive, 
+   [ip_vars] contains the names of the type variables surviving in ML, 
+   [ip_types] contains the ML types of all constructors.    
+*)
 
-type ml_ind = 
-  ml_one_ind list * bool (* cofix *)  
+type ml_ind_packet = { 
+  ip_logical : bool;
+  ip_sign : signature; 
+  ip_vars : identifier list; 
+  ip_types : (ml_type list) array }  
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type ml_ind = {
+  ind_info : inductive_info;
+  ind_nparams : int; 	       
+  ind_packets : ml_ind_packet array }
 
 (*s ML terms. *)
 
@@ -59,11 +85,10 @@ type ml_ast =
   | MLmagic  of ml_ast
   | MLcustom of string
 
-
 (*s ML declarations. *)
 
 type ml_decl = 
-  | Dind  of ml_ind
+  | Dind  of kernel_name * ml_ind
   | Dtype of global_reference * identifier list * ml_type
   | Dterm   of global_reference * ml_ast * ml_type
   | DcustomTerm of global_reference * string
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 07df294b51..07bf98aeea 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -409,10 +409,9 @@ let rec type_search t = function
 
 let decl_type_search t l = 
   let one_decl = function 
-    | Dind(l,_) -> 
-	List.iter (fun (_,_,l) -> 
-		    (List.iter (fun (_,l) -> 
-				  List.iter (type_search t) l) l)) l
+    | Dind (_,{ind_packets=p})  -> 
+	Array.iter 
+	  (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
     | Dterm (_,_,u) -> type_search t u
     | Dfix (_,_,v) -> Array.iter (type_search t) v
     | Dtype (_,_,u) -> type_search t u
@@ -1205,19 +1204,19 @@ let ast_iter_references do_term do_cons do_type a =
       | MLcast (_,t) -> type_iter_references do_type t 
       | _ -> ()
   in iter a
-
+  
 let decl_iter_references do_term do_cons do_type = 
   let type_iter = type_iter_references do_type 
   and ast_iter = ast_iter_references do_term do_cons do_type in 
-  let cons_iter (r,l) = do_cons r; List.iter type_iter l in 
-  let ind_iter (_,r,l) = 
-    do_type r; 
-    (try List.iter do_term (find_proj ((kn_of_r r),0)) 
-     with Not_found -> ()); 
-    List.iter cons_iter l 
+  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
+  let packet_iter ip p = 
+    do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in
+  let ind_iter kn ind =
+    if ind.ind_info = Record then List.iter do_term (find_projections kn); 
+    Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
   in 
   function 
-    | Dind (l,_) -> List.iter ind_iter l 
+    | Dind (kn,ind) -> ind_iter kn ind 
     | Dtype (r,_,t) -> do_type r; type_iter t 
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
     | Dfix(rv,c,t) -> 	
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2e81a52c9e..f168c57b80 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -198,7 +198,7 @@ let rec pp_expr par env args =
 		(hov 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ 
 		 spc () ++ str "in") ++ 
 	      spc () ++ hov 0 pp_a2))
-    | MLglob r when is_proj r && args <> [] ->
+    | MLglob r when is_projection r && args <> [] ->
 	let record = List.hd args in 
 	pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
     | MLglob r -> 
@@ -210,13 +210,13 @@ let rec pp_expr par env args =
 	else pp_global r
     | MLcons (r,args') -> 
 	(try 
-	   let projs = find_proj (kn_of_r r, 0) in 
+	   let projs = find_projections (kn_of_r r) in 
 	   pp_record_pat (projs, List.map (pp_expr true env []) args')
 	 with Not_found ->
 	   assert (args=[]);
 	   let tuple = pp_tuple (pp_expr true env []) args' in 
 	   if Refset.mem r !cons_cofix then 
-	     pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++ str ")")
+	     pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
 	   else pp_par par (pp_global r ++ spc () ++ tuple))
     | MLcase (t, pv) ->
 	let r,_,_ = pv.(0) in 
@@ -226,7 +226,7 @@ let rec pp_expr par env args =
 	  (pp_expr false env [] t) 
 	in 
 	let record = 
-	  try ignore (find_proj (kn_of_r r, 0)); true with Not_found -> false
+	  try ignore (find_projections (kn_of_r r)); true with Not_found -> false
 	in 
 	if Array.length pv = 1 && not record then 
 	  let s1,s2 = pp_one_pat env pv.(0) in 
@@ -269,7 +269,7 @@ and pp_one_pat env (r,ids,t) =
   let ids,env' = push_vars (List.rev ids) env in
   let expr = pp_expr (expr_needs_par t) env' [] t in 
   try 
-    let projs = find_proj (kn_of_r r,0) in 
+    let projs = find_projections (kn_of_r r) in 
     pp_record_pat (projs, List.rev_map pr_id ids), expr
   with Not_found -> 
     let args = 
@@ -340,64 +340,79 @@ let pp_Dfix env (p,c,t) =
 let pp_parameters l = 
   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
 
-let pp_one_ind prefix (pl,name,cl) =
+let pp_one_ind prefix ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
-    (pp_global r ++
-     match l with
-       | [] -> (mt ()) 
-       | _  -> (str " of " ++
-      		prlist_with_sep 
-		  (fun () -> (spc () ++ str "* ")) 
-		  (pp_type true pl) l))
+    hov 2 (str "  | " ++ pp_global r ++
+	   match l with
+	     | [] -> mt () 
+	     | _  -> (str " of " ++ 
+		      prlist_with_sep 
+			(fun () -> spc () ++ str "* ") (pp_type true pl) l))
   in
-  (pp_parameters pl ++ str prefix ++ pp_global name ++ str " =" ++ 
-   if cl = [] then str " unit (* empty inductive *)" 
-   else (fnl () ++
-	 v 0 (str "  | " ++
-	      prlist_with_sep (fun () -> (fnl () ++ str "  | "))
-                (fun c -> hov 2 (pp_constructor c)) cl)))
-
-let pp_ind il =
-  str "type " ++
-  prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "") il
-  ++ fnl ()
-
-let pp_record ip pl l = 
-  let pl = rename_tvars keywords pl in 
-  str "type " ++ pp_parameters pl ++ pp_global (IndRef ip) ++ str " = { "++
+  pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ 
+  if cv = [||] then str " unit (* empty inductive *)" 
+  else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
+			(Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
+
+let pp_comment s = str "(* " ++ s ++ str " *)" ++ fnl ()
+
+let pp_logical_ind ip packet = 
+  pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+  pp_comment (str "with constructors : " ++ 
+	      prvect_with_sep spc Printer.pr_global 
+		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
+    
+let pp_singleton kn packet = 
+  let l = rename_tvars keywords packet.ip_vars in 
+  hov 0 (str "type " ++ spc () ++ pp_parameters l ++
+	 pp_global (IndRef (kn,0)) ++ spc () ++ str "=" ++ spc () ++
+	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
+	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+		     Printer.pr_global (ConstructRef ((kn,0),1))))
+
+let pp_record kn packet = 
+  let l = List.combine (find_projections kn) packet.ip_types.(0) in 
+  let projs = find_projections kn in
+  let pl = rename_tvars keywords packet.ip_vars in 
+  str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
-	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l)
+	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) 
   ++ str " }" ++ fnl () 
 
-let pp_coind_preamble (pl,name,_) = 
+let pp_coind ip pl = 
+  let r = IndRef ip in 
   let pl = rename_tvars keywords pl in
-  pp_parameters pl ++ pp_global name ++ str " = " ++ 
-  pp_parameters pl ++ str "__" ++ pp_global name ++ str " Lazy.t"
-
-let pp_coind il = 
-  str "type " ++ 
-  prlist_with_sep (fun () -> fnl () ++ str "and ") pp_coind_preamble il ++
-  fnl () ++ str "and " ++ 
-  prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "__") il ++
-  fnl ()
+  pp_parameters pl ++ pp_global r ++ str " = " ++ 
+  pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
+
+let rec pp_ind co first kn i ind =
+  if i >= Array.length ind.ind_packets then mt () 
+  else 
+    let ip = (kn,i) in 
+    let p = ind.ind_packets.(i) in 
+    if p.ip_logical then  
+      pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
+    else 
+      str (if first then "type " else "and ") ++
+      (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ 
+      pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+      fnl () ++ pp_ind co false kn (i+1) ind
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dind ([], _) -> mt ()
-  | Dind (i, true) -> 
-      List.iter   
-	(fun (_,_,l) -> 
-	   List.iter (fun (r,_) -> 
-			cons_cofix := Refset.add r !cons_cofix)  l) i; 
-      hov 0 (pp_coind i)
-  | Dind ([vl, IndRef ip, [_,l]] as i, _) -> 
-      (try 
-	 let projs = find_proj ip in 
-	 hov 0 (pp_record ip vl (List.combine projs l))
-       with Not_found -> hov 0 (pp_ind i)) 
-  | Dind (i,_) -> hov 0 (pp_ind i)
+  | Dind (kn,i) as d -> 
+      (match i.ind_info with 
+	 | Singleton -> pp_singleton kn i.ind_packets.(0) 
+	 | Record -> pp_record kn i.ind_packets.(0)
+	 | Coinductive -> 
+	     let nop _ = () 
+	     and add r = cons_cofix := Refset.add r !cons_cofix in 
+	     decl_iter_references nop add nop d; 
+	     hov 0 (pp_ind true true kn 0 i)
+	 | Standard -> 
+	     hov 0 (pp_ind false true kn 0 i))
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in 
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
@@ -407,7 +422,7 @@ let pp_decl = function
       (* We compute renamings of [rv] before asking [empty_env ()]... *)
       let ppv = Array.map pp_global rv in 
       hov 0 (pp_Dfix (empty_env ()) (ppv,defs,typs))
-  | Dterm (r, a, t) when is_proj r -> 
+  | Dterm (r, a, t) when is_projection r -> 
       let e = pp_global r in 
       (pp_val e t ++ 
        hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl())) 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 75c70fd7f2..223bc77b38 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -17,32 +17,48 @@ open Goptions
 open Libnames
 open Util
 open Pp
+open Miniml
 
+(*S Warning and Error messages. *)
 
-(*s Warning and Error messages. *)
-
-let error_axiom_scheme kn = 
-  errorlabstrm "axiom_scheme_message" 
+let error_axiom_scheme r = 
+  errorlabstrm "Extraction" 
     (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-     Printer.pr_global (ConstRef kn) ++ spc () ++ str ".") 
+     Printer.pr_global r ++ spc () ++ str ".") 
 
-let error_axiom kn =
-  errorlabstrm "axiom_message"
+let error_axiom r =
+  errorlabstrm "Extraction"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-     Printer.pr_global (ConstRef kn) ++ spc () ++ str "first.")
+     Printer.pr_global r ++ spc () ++ str "first.")
 
-let warning_axiom kn = 
+let warning_axiom r = 
   Options.if_verbose warn 
     (str "This extraction depends on logical axiom" ++ spc () ++ 
-     Printer.pr_global (ConstRef kn) ++ str "." ++ spc() ++ 
+     Printer.pr_global r ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
      spc () ++ str "may lead to incorrect or non-terminating ML terms.")
     
 let error_section () = 
-  errorlabstrm "section_message"
+  errorlabstrm "Extraction"
     (str "You can't do that within a section. Close it and try again.")
 
-(*s AutoInline parameter *)
+let error_constant r = 
+  errorlabstrm "Extraction"
+    (Printer.pr_global r ++ spc () ++ str "is not a constant.") 
+
+let error_type_scheme r = 
+  errorlabstrm "Extraction"
+    (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.")
+
+let error_inductive r = 
+  errorlabstrm "Extraction"
+    (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+
+let error_nb_cons () = 
+  errorlabstrm "Extraction" (str "Not the right number of constructors.")
+
+
+(*S Extraction AutoInline *)
 
 let auto_inline_ref = ref true
 
@@ -55,7 +71,8 @@ let _ = declare_bool_option
 	   optread = auto_inline; 
 	   optwrite = (:=) auto_inline_ref}
 
-(*s Optimize parameter *)
+
+(*S Extraction Optimize *)
 
 let optim_ref = ref true
 
@@ -68,18 +85,8 @@ let _ = declare_bool_option
 	   optread = optim; 
 	   optwrite = (:=) optim_ref}
 
-(*s Auxiliary functions *) 
 
-let is_constant r = match r with 
-  | ConstRef _ -> true
-  | _ -> false
-
-let check_constant r = 
-  if (is_constant r) then r 
-  else errorlabstrm "extract_constant"
-	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
-
-(*s Target Language *)
+(*S Extraction Lang *)
 
 type lang = Ocaml | Haskell | Scheme | Toplevel
 
@@ -102,7 +109,8 @@ let _ = declare_summary "Extraction Lang"
 
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
-(*s Table for custom inlining *)
+
+(*S Extraction Inline/NoInline *)
 
 let empty_inline_table = (Refset.empty,Refset.empty)
 
@@ -138,14 +146,15 @@ let _ = declare_summary "Extraction Inline"
 
 let extraction_inline b l =
   if Lib.sections_are_opened () then error_section (); 
-  let refs = List.map (fun x -> check_constant (Nametab.global x)) l in 
+  let refs = List.map Nametab.global l in 
+  List.iter (function  ConstRef _ -> () | r -> error_constant r) refs; 
   Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
 (*s Printing part *)
 
 let print_extraction_inline () = 
   let (i,n)= !inline_table in 
-  let i'= Refset.filter is_constant i in 
+  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in 
   msg 
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
@@ -167,7 +176,8 @@ let (reset_inline,_) =
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
-(*s Table for direct ML extractions. *)
+
+(*S Extract Constant/Inductive. *)
 
 type kind = Term | Type | Ind | Construct 
 
@@ -176,15 +186,11 @@ let check_term_or_type r = match r with
       let env = Global.env () in 
       let typ = Environ.constant_type env sp in 
       let typ = Reduction.whd_betadeltaiota env typ in
-      (match kind_of_term typ with 
-	 | Sort _ -> (r,Type)
-	 | _ -> if not (Reduction.is_arity env typ) then (r,Term)
-	   else errorlabstrm "extract_constant"
-	     (Printer.pr_global r ++ spc () ++ 
-	      str "is a type scheme, not a type."))
-  | _ -> errorlabstrm "extract_constant"
-	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
-
+      if isSort typ then (r,Type) 
+      else if Reduction.is_arity env typ then error_type_scheme r
+      else (r,Term)
+  | _ -> error_constant r
+	
 let empty_extractions = (Refmap.empty, Refset.empty)
 
 let extractions = ref empty_extractions
@@ -222,7 +228,6 @@ let _ = declare_summary "ML extractions"
 	    init_function = (fun () -> extractions := empty_extractions);
 	    survive_section = true }
 
-
 (*s Grammar entries. *)
 
 let extract_constant_inline inline r s =
@@ -237,8 +242,7 @@ let extract_inductive r (s,l) =
   | IndRef ((kn,i) as ip) ->
       let mib = Global.lookup_mind kn in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
-      if n <> List.length l then
-	error "Not the right number of constructors.";
+      if n <> List.length l then error_nb_cons (); 
       Lib.add_anonymous_leaf (inline_extraction (true,[g]));
       Lib.add_anonymous_leaf (in_ml_extraction (g,Ind,s));
       list_iter_i
@@ -246,31 +250,26 @@ let extract_inductive r (s,l) =
 	   let g = ConstructRef (ip,succ j) in 
 	   Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	   Lib.add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
-  | _ -> 
-      errorlabstrm "extract_inductive"
-	(Printer.pr_global g ++ spc () ++ str "is not an inductive type.")
+  | _ -> error_inductive g 
 
-(*s Record Inductive tables. *)
 
-let record_type_table = 
-  ref (Gmap.empty : (inductive, global_reference list) Gmap.t)
+(*S The other tables: constants, inductives, records, ... *)
 
-let record_proj_table = ref Refset.empty
+(*s Constants tables. *) 
 
-let add_record i l = 
-  record_type_table := Gmap.add i l !record_type_table; 
-  record_proj_table := List.fold_right Refset.add l !record_proj_table
+let terms = ref (KNmap.empty : ml_decl KNmap.t)
+let add_term kn d = terms := KNmap.add kn d !terms
+let lookup_term kn = KNmap.find kn !terms
 
-let find_proj i = Gmap.find i !record_type_table
+let types = ref (KNmap.empty : ml_schema KNmap.t)
+let add_type kn s = types := KNmap.add kn s !types
+let lookup_type kn = KNmap.find kn !types 
 
-let is_proj r = Refset.mem r !record_proj_table 
+(*s Inductives table. *)
 
-let _ = declare_summary "Extraction Record tables"
-	  { freeze_function = (fun () -> !record_type_table,!record_proj_table); 
-	    unfreeze_function = 
-	      (fun (x,y) -> record_type_table := x; record_proj_table := y); 
-	    init_function = (fun () -> ()); 
-	    survive_section = true }
+let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let add_ind kn m = inductives := KNmap.add kn m !inductives
+let lookup_ind kn = KNmap.find kn !inductives
 
 (*s Recursors table. *)
 
@@ -291,9 +290,32 @@ let is_recursor = function
   | ConstRef kn -> KNset.mem kn !recursors
   | _ -> false
 
-let _ = declare_summary "Extraction Recursors table"
-	  { freeze_function = (fun () -> !recursors); 
-	    unfreeze_function = (fun x -> recursors := x);
-	    init_function = (fun () -> ()); 
+(*s Record tables. *)
+
+let records = ref (KNmap.empty : global_reference list KNmap.t)
+let projs = ref Refset.empty
+
+let add_record kn l = 
+  records := KNmap.add kn l !records; 
+  projs := List.fold_right Refset.add l !projs
+
+let find_projections kn = KNmap.find kn !records
+let is_projection r = Refset.mem r !projs
+
+(*s Tables synchronization. *)
+
+let freeze () = !terms, !types, !inductives, !recursors, !records, !projs
+
+let unfreeze (te,ty,id,re,rd,pr) = 
+  terms:=te; types:=ty; inductives:=id; recursors:=re; records:=rd; projs:=pr
+
+let _ = declare_summary "Extraction tables"
+	  { freeze_function = freeze;
+	    unfreeze_function = unfreeze;
+	    init_function = (fun () -> ());
 	    survive_section = true }
 
+
+
+
+
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 3ffb74ac4b..e6495add6e 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -10,16 +10,18 @@
 
 open Names
 open Libnames
+open Miniml
 
 (*s Warning and Error messages. *)
 
+val error_axiom_scheme : global_reference -> 'a
+val error_axiom : global_reference -> 'a
+val warning_axiom : global_reference -> unit
 val error_section : unit -> 'a
-
-val error_axiom_scheme : kernel_name -> 'a
-
-val error_axiom : kernel_name -> 'a
-
-val warning_axiom : kernel_name -> unit
+val error_constant : global_reference -> 'a
+val error_type_scheme : global_reference -> 'a
+val error_inductive : global_reference -> 'a
+val error_nb_cons : unit -> 'a
 
 (*s AutoInline parameter *) 
 
@@ -32,46 +34,46 @@ val optim :  unit -> bool
 (*s Target language. *)
 
 type lang = Ocaml | Haskell | Scheme | Toplevel
-
 val lang : unit -> lang 
 
 (*s Table for custom inlining *) 
 
 val to_inline : global_reference -> bool
-
 val to_keep : global_reference -> bool
 
 (*s Table for direct ML extractions. *)
 
 val is_ml_extraction : global_reference -> bool
-
 val find_ml_extraction : global_reference -> string
-
 val ml_extractions : unit -> Refset.t
-
 val ml_type_extractions : unit -> (global_reference * string) list
-
 val ml_term_extractions : unit -> (global_reference * string) list
 
 (*s Extraction commands. *)
 
 val extraction_language : lang -> unit
-
 val extraction_inline : bool -> reference list -> unit
-
 val print_extraction_inline : unit -> unit
-
 val reset_extraction_inline : unit -> unit
-
 val extract_constant_inline : bool -> reference -> string -> unit
-
 val extract_inductive : reference -> string * string list -> unit
 
-(*s some tables. *)
+(*s Some table-related operations *)
+
+val add_term : kernel_name -> ml_decl -> unit
+val lookup_term : kernel_name -> ml_decl
 
-val add_record : inductive -> global_reference list -> unit
-val find_proj : inductive -> global_reference list
-val is_proj : global_reference -> bool 
+val add_type : kernel_name -> ml_schema -> unit
+val lookup_type : kernel_name -> ml_schema
+
+val add_ind : kernel_name -> ml_ind -> unit
+val lookup_ind : kernel_name -> ml_ind
 
 val add_recursors : kernel_name -> unit
 val is_recursor : global_reference -> bool 
+
+val add_record : kernel_name -> global_reference list -> unit
+val find_projections : kernel_name -> global_reference list
+val is_projection : global_reference -> bool 
+
+
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 33e832af43..8c706cdf80 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -293,7 +293,7 @@ type 'x truc =
 
 Definition test24:= (sigT Set [a:Set](option a)).
 Extraction test24.
-(* type test24 = (unit, Obj.t option) sigT *)
+(* type test24 = (__, __ option) sigT *)
 
 
 (** Coq term non strongly-normalizable after extraction *)