Diverses petites simplications de la machine de preuves.

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

16 files changed, 333 insertions, 515 deletions

diff --git a/.depend b/.depend
index 1b9601c88..83fcf1044 100644
--- a/.depend
+++ b/.depend
@@ -24,8 +24,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/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 +46,8 @@ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 library/opaque.cmi: kernel/closure.cmi kernel/environ.cmi kernel/names.cmi \
     kernel/safe_typing.cmi 
 library/summary.cmi: kernel/names.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -225,18 +225,18 @@ toplevel/recordobj.cmi: library/nametab.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/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     library/nametab.cmi proofs/proof_type.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 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 
@@ -419,32 +419,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/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/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi library/global.cmi library/impargs.cmi \
     kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \
@@ -513,10 +505,12 @@ library/nametab.cmx: kernel/declarations.cmx kernel/environ.cmx \
     lib/util.cmx library/nametab.cmi 
 library/opaque.cmo: kernel/closure.cmi kernel/declarations.cmi \
     kernel/environ.cmi library/global.cmi kernel/names.cmi \
-    library/summary.cmi kernel/term.cmi lib/util.cmi library/opaque.cmi 
+    library/nametab.cmi lib/pp.cmi library/summary.cmi kernel/term.cmi \
+    lib/util.cmi library/opaque.cmi 
 library/opaque.cmx: kernel/closure.cmx kernel/declarations.cmx \
     kernel/environ.cmx library/global.cmx kernel/names.cmx \
-    library/summary.cmx kernel/term.cmx lib/util.cmx library/opaque.cmi 
+    library/nametab.cmx lib/pp.cmx library/summary.cmx kernel/term.cmx \
+    lib/util.cmx library/opaque.cmi 
 library/states.cmo: library/lib.cmi library/library.cmi library/summary.cmi \
     lib/system.cmi library/states.cmi 
 library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
@@ -525,6 +519,14 @@ 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/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/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \
@@ -914,14 +916,16 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/inductive.cmx \
 proofs/clenv.cmo: kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi pretyping/instantiate.cmi \
     proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    proofs/refiner.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
     pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi 
 proofs/clenv.cmx: kernel/environ.cmx proofs/evar_refiner.cmx \
     pretyping/evarutil.cmx pretyping/evd.cmx pretyping/instantiate.cmx \
     proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
+    proofs/refiner.cmx pretyping/retyping.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi 
 proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
@@ -954,17 +958,17 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \
     lib/util.cmx proofs/logic.cmi 
 proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \
-    library/declare.cmi lib/edit.cmi kernel/environ.cmi pretyping/evd.cmi \
-    library/lib.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    proofs/pfedit.cmi 
+    library/declare.cmi lib/edit.cmi kernel/environ.cmi \
+    proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi 
 proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \
-    library/declare.cmx lib/edit.cmx kernel/environ.cmx pretyping/evd.cmx \
-    library/lib.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    proofs/pfedit.cmi 
+    library/declare.cmx lib/edit.cmx kernel/environ.cmx \
+    proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi 
 proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \
     pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \
@@ -1022,19 +1026,19 @@ proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
     kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacinterp.cmi 
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
-    kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \
-    proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
+    kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
+    library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi \
+    kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
+    kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/tacmach.cmi 
 proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
-    kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \
-    proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    proofs/refiner.cmx kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
+    kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
+    library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx \
+    kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
+    kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
 proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
@@ -1110,17 +1114,17 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
 tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \
-    pretyping/evarutil.cmi pretyping/evd.cmi lib/explore.cmi proofs/logic.cmi \
-    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+    lib/explore.cmi proofs/logic.cmi kernel/names.cmi pretyping/pattern.cmi \
+    lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi 
 tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
-    pretyping/evarutil.cmx pretyping/evd.cmx lib/explore.cmx proofs/logic.cmx \
-    kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
+    lib/explore.cmx proofs/logic.cmx kernel/names.cmx pretyping/pattern.cmx \
+    lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx 
 tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
     tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
     kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \
@@ -1263,10 +1267,12 @@ tactics/setoid_replace.cmx: parsing/astterm.cmx tactics/auto.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
     tactics/setoid_replace.cmi 
-tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi 
-tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi 
+tactics/tacentries.cmo: proofs/evar_refiner.cmi proofs/proof_trees.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    tactics/tacentries.cmi 
+tactics/tacentries.cmx: proofs/evar_refiner.cmx proofs/proof_trees.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    tactics/tacentries.cmi 
 tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi library/global.cmi pretyping/indrec.cmi \
@@ -1327,12 +1333,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.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/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
@@ -1511,52 +1517,42 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.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/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/vernacinterp.cmx \
-    toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
     parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
-    toplevel/discharge.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi parsing/extend.cmi library/global.cmi \
-    library/goptions.cmi library/impargs.cmi pretyping/inductiveops.cmi \
-    library/lib.cmi library/library.cmi toplevel/metasyntax.cmi \
-    toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi library/opaque.cmi lib/options.cmi proofs/pfedit.cmi \
-    lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
-    toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
-    parsing/search.cmi library/states.cmi pretyping/syntax_def.cmi \
-    lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
-    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
-    kernel/typeops.cmi kernel/univ.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernacentries.cmi 
+    toplevel/discharge.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
+    pretyping/evarutil.cmi pretyping/evd.cmi parsing/extend.cmi \
+    library/global.cmi library/goptions.cmi library/impargs.cmi \
+    pretyping/inductiveops.cmi library/lib.cmi library/library.cmi \
+    toplevel/metasyntax.cmi toplevel/mltop.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi library/opaque.cmi lib/options.cmi \
+    proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    toplevel/record.cmi toplevel/recordobj.cmi proofs/refiner.cmi \
+    kernel/safe_typing.cmi parsing/search.cmi library/states.cmi \
+    pretyping/syntax_def.cmi lib/system.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
+    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
+    pretyping/termops.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
-    toplevel/discharge.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx parsing/extend.cmx library/global.cmx \
-    library/goptions.cmx library/impargs.cmx pretyping/inductiveops.cmx \
-    library/lib.cmx library/library.cmx toplevel/metasyntax.cmx \
-    toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx library/opaque.cmx lib/options.cmx proofs/pfedit.cmx \
-    lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
-    toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
-    parsing/search.cmx library/states.cmx pretyping/syntax_def.cmx \
-    lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
-    kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
-    kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernacentries.cmi 
+    toplevel/discharge.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
+    pretyping/evarutil.cmx pretyping/evd.cmx parsing/extend.cmx \
+    library/global.cmx library/goptions.cmx library/impargs.cmx \
+    pretyping/inductiveops.cmx library/lib.cmx library/library.cmx \
+    toplevel/metasyntax.cmx toplevel/mltop.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx library/opaque.cmx lib/options.cmx \
+    proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    toplevel/record.cmx toplevel/recordobj.cmx proofs/refiner.cmx \
+    kernel/safe_typing.cmx parsing/search.cmx library/states.cmx \
+    pretyping/syntax_def.cmx lib/system.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
+    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
+    pretyping/termops.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -1567,18 +1563,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmi 
-contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
-    library/declare.cmi pretyping/detyping.cmi kernel/indtypes.cmi \
-    kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
-    contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
-    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
-    lib/util.cmi contrib/correctness/pcic.cmi 
-contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
-    library/declare.cmx pretyping/detyping.cmx kernel/indtypes.cmx \
-    kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
-    contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
-    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
-    lib/util.cmx contrib/correctness/pcic.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/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/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 \
@@ -1591,6 +1585,18 @@ contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.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 kernel/indtypes.cmi \
+    kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
+    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
+    lib/util.cmi contrib/correctness/pcic.cmi 
+contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
+    library/declare.cmx pretyping/detyping.cmx kernel/indtypes.cmx \
+    kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
+    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
+    lib/util.cmx contrib/correctness/pcic.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 \
@@ -2027,6 +2033,14 @@ contrib/interface/pbp.cmx: parsing/coqlib.cmx contrib/interface/ctast.cmx \
     kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
     tactics/tacticals.cmx tactics/tactics.cmx kernel/term.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 library/global.cmi \
@@ -2047,14 +2061,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/term.cmx parsing/termast.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 \
@@ -2151,8 +2157,6 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     parsing/printer.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 \
@@ -2173,6 +2177,8 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.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
 contrib/correctness/psyntax.cmo: parsing/grammar.cma
 contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
diff --git a/.depend.coq b/.depend.coq
index 1a773e932..41dcf0180 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,269 +1,166 @@
-theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
-theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo
-theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
-theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
-theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
-theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo
-theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
-theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
-theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
+contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo
+contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
+contrib/interface/Centaur.vo: contrib/interface/Centaur.v
+contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
+contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
+contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
+contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/ZArith/ZArith.vo theories/Bool/Sumbool.vo
+contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
+contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
+contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
+contrib/xml/Xml.vo: contrib/xml/Xml.v
+contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
+contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
+contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
+contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
+contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo
+contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/Quote.vo: contrib/ring/Quote.v
+contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
+contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
+contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
+contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
+contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo
+contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
+contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
+contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/OmegaSyntax.vo
+theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
+theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
+theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
+theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo contrib/omega/Zpower.vo
+theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
+theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
+theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
+theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
+theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith.vo theories/Reals/TypeSyntax.vo
+theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
+theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theories/Logic/Eqdep.vo
 theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo
 theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
-theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v
 theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo
 theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo
-theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
-theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
-theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
-theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
-theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
-theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
-theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
-theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
-theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
-theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
-theories/Sets/Permut.vo: theories/Sets/Permut.v
-theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
-theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
-theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
-theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
-theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
-theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
-theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
-theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
-theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
-theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
-theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
-theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v tactics/Setoid_replace.vo
 theories/Relations/Rstar.vo: theories/Relations/Rstar.v
 theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo
 theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo
 theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
 theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
-theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
-theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo contrib/omega/Zpower.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith.vo theories/Reals/TypeSyntax.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
-theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
-theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
-theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
-theories/Num/SubProps.vo: theories/Num/SubProps.v
-theories/Num/Params.vo: theories/Num/Params.v
-theories/Num/OppProps.vo: theories/Num/OppProps.v
-theories/Num/OppAxioms.vo: theories/Num/OppAxioms.v
-theories/Num/NSyntax.vo: theories/Num/NSyntax.v theories/Num/Leibniz/Params.vo
-theories/Num/NeqProps.vo: theories/Num/NeqProps.v theories/Num/NeqParams.vo theories/Num/NeqAxioms.vo theories/Num/EqParams.vo theories/Num/Leibniz/EqAxioms.vo
-theories/Num/NeqParams.vo: theories/Num/NeqParams.v theories/Num/Leibniz/Params.vo
-theories/Num/NeqDef.vo: theories/Num/NeqDef.v theories/Num/Leibniz/Params.vo theories/Num/EqParams.vo theories/Num/Leibniz/EqAxioms.vo
-theories/Num/NeqAxioms.vo: theories/Num/NeqAxioms.v theories/Num/EqParams.vo theories/Num/NeqParams.vo
-theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Nat/Axioms.vo theories/Num/AddProps.vo theories/Num/NeqProps.vo
-theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo
-theories/Num/LeAxioms.vo: theories/Num/LeAxioms.v theories/Num/Nat/Axioms.vo theories/Num/LtProps.vo
-theories/Num/GtProps.vo: theories/Num/GtProps.v
-theories/Num/GtAxioms.vo: theories/Num/GtAxioms.v theories/Num/Nat/Axioms.vo theories/Num/LeProps.vo
-theories/Num/GeProps.vo: theories/Num/GeProps.v
-theories/Num/GeAxioms.vo: theories/Num/GeAxioms.v theories/Num/Nat/Axioms.vo theories/Num/LtProps.vo
-theories/Num/EqParams.vo: theories/Num/EqParams.v theories/Num/Leibniz/Params.vo
-theories/Num/EqAxioms.vo: theories/Num/EqAxioms.v theories/Num/Leibniz/Params.vo theories/Num/EqParams.vo theories/Num/Nat/NSyntax.vo
-theories/Num/DiscrProps.vo: theories/Num/DiscrProps.v theories/Num/DiscrAxioms.vo theories/Num/LtProps.vo
-theories/Num/DiscrAxioms.vo: theories/Num/DiscrAxioms.v theories/Num/Leibniz/Params.vo theories/Num/Nat/NSyntax.vo
-theories/Num/Definitions.vo: theories/Num/Definitions.v
-theories/Num/Axioms.vo: theories/Num/Axioms.v theories/Num/Leibniz/Params.vo theories/Num/EqParams.vo theories/Num/Nat/NSyntax.vo
-theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Nat/Axioms.vo theories/Num/Leibniz/EqAxioms.vo
-theories/Logic/JMeq.vo: theories/Logic/JMeq.v
-theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
-theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v theories/Logic/Elimdep.vo
-theories/Logic/Elimdep.vo: theories/Logic/Elimdep.v
-theories/Logic/Decidable.vo: theories/Logic/Decidable.v
-theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
-theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
-theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
-theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
-theories/Logic/Berardi.vo: theories/Logic/Berardi.v theories/Logic/Elimdep.vo
-theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
-theories/Lists/Streams.vo: theories/Lists/Streams.v
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.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/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo
-theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo
-theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
-theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo
-theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo
-theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
-theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
-theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
 theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
+theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo
 theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo
+theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
 theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo
+theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo
 theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo
+theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo
 theories/IntMap/Adist.vo: theories/IntMap/Adist.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/Arith/Min.vo theories/IntMap/Addr.vo
+theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
 theories/IntMap/Addr.vo: theories/IntMap/Addr.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo
+theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
 theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo
+theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
 theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
-theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
-theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
-theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
-theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo
-theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
-theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
-theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
-theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
-theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
-theories/Init/Datatypes.vo: theories/Init/Datatypes.v
-theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
-theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
+theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
+theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
+theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
+theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
+theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
+theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
+theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
+theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
+theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
+theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
+theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
+theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
+theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
+theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
+theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
+theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
+theories/Sets/Permut.vo: theories/Sets/Permut.v
+theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
+theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
+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/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
+theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo
+theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo
+theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
+theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
+theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
+theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
+theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
-theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/DecBool.vo: theories/Bool/DecBool.v
+theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
+theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
-theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
+theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable.vo
+theories/Arith/EqNat.vo: theories/Arith/EqNat.v
+theories/Arith/Even.vo: theories/Arith/Even.v
 theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo theories/Arith/Lt.vo
-theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
-theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
-theories/Arith/Le.vo: theories/Arith/Le.v
-theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
-theories/Arith/Even.vo: theories/Arith/Even.v
-theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
-theories/Arith/EqNat.vo: theories/Arith/EqNat.v
-theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Compare_dec.vo
 theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
-theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Logic/Decidable.vo
+theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
+theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
-test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
-test-suite/success/unfold.vo: test-suite/success/unfold.v
-test-suite/success/Tauto.vo: test-suite/success/Tauto.v
-test-suite/success/mutual_ind.vo: test-suite/success/mutual_ind.v theories/Lists/PolyList.vo
-test-suite/success/induct.vo: test-suite/success/induct.v theories/Lists/PolyList.vo
-test-suite/success/inds_type_sec.vo: test-suite/success/inds_type_sec.v
-test-suite/success/Hints.vo: test-suite/success/Hints.v
-test-suite/success/Fourier.vo: test-suite/success/Fourier.v theories/Reals/SplitAbsolu.vo contrib/fourier/Fourier.vo
-test-suite/success/fix.vo: test-suite/success/fix.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-test-suite/success/Field.vo: test-suite/success/Field.v theories/Reals/Reals.vo
-test-suite/success/evars.vo: test-suite/success/evars.v
-test-suite/success/eqdecide.vo: test-suite/success/eqdecide.v
-test-suite/success/eauto.vo: test-suite/success/eauto.v theories/Lists/PolyList.vo
-test-suite/success/DiscrR.vo: test-suite/success/DiscrR.v theories/Reals/Reals.vo theories/Reals/DiscrR.vo
-test-suite/success/Decompose.vo: test-suite/success/Decompose.v
-test-suite/success/Check.vo: test-suite/success/Check.v
-test-suite/success/Cases.vo: test-suite/success/Cases.v theories/Bool/Bool.vo theories/Arith/Peano_dec.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo
-test-suite/success/CasesDep.vo: test-suite/success/CasesDep.v theories/Init/Prelude.vo theories/Init/Logic_TypeSyntax.vo theories/Init/Logic_Type.vo
-test-suite/success/Case9.vo: test-suite/success/Case9.v
-test-suite/success/Case8.vo: test-suite/success/Case8.v
-test-suite/success/Case7.vo: test-suite/success/Case7.v
-test-suite/success/Case6.vo: test-suite/success/Case6.v
-test-suite/success/Case5.vo: test-suite/success/Case5.v
-test-suite/success/Case4.vo: test-suite/success/Case4.v
-test-suite/success/Case3.vo: test-suite/success/Case3.v
-test-suite/success/Case2.vo: test-suite/success/Case2.v
-test-suite/success/Case1.vo: test-suite/success/Case1.v
-test-suite/success/Case11.vo: test-suite/success/Case11.v
-test-suite/success/Case10.vo: test-suite/success/Case10.v
-test-suite/success/Apply.vo: test-suite/success/Apply.v
-test-suite/failure/universes.vo: test-suite/failure/universes.v
-test-suite/failure/universes-sections2.vo: test-suite/failure/universes-sections2.v
-test-suite/failure/universes-sections1.vo: test-suite/failure/universes-sections1.v
-test-suite/failure/universes-buraliforti.vo: test-suite/failure/universes-buraliforti.v
-test-suite/failure/Tauto.vo: test-suite/failure/Tauto.v
-test-suite/failure/search.vo: test-suite/failure/search.v
-test-suite/failure/redef.vo: test-suite/failure/redef.v
-test-suite/failure/positivity.vo: test-suite/failure/positivity.v
-test-suite/failure/params_ind.vo: test-suite/failure/params_ind.v
-test-suite/failure/illtype1.vo: test-suite/failure/illtype1.v
-test-suite/failure/fixpoint1.vo: test-suite/failure/fixpoint1.v
-test-suite/failure/clash_cons.vo: test-suite/failure/clash_cons.v
-test-suite/failure/check.vo: test-suite/failure/check.v
-test-suite/failure/Case9.vo: test-suite/failure/Case9.v
-test-suite/failure/Case8.vo: test-suite/failure/Case8.v
-test-suite/failure/Case7.vo: test-suite/failure/Case7.v
-test-suite/failure/Case6.vo: test-suite/failure/Case6.v
-test-suite/failure/Case5.vo: test-suite/failure/Case5.v
-test-suite/failure/Case4.vo: test-suite/failure/Case4.v
-test-suite/failure/Case3.vo: test-suite/failure/Case3.v
-test-suite/failure/Case2.vo: test-suite/failure/Case2.v
-test-suite/failure/Case1.vo: test-suite/failure/Case1.v
-test-suite/failure/Case14.vo: test-suite/failure/Case14.v
-test-suite/failure/Case13.vo: test-suite/failure/Case13.v
-test-suite/failure/Case12.vo: test-suite/failure/Case12.v
-test-suite/failure/Case11.vo: test-suite/failure/Case11.v
-test-suite/failure/Case10.vo: test-suite/failure/Case10.v
-test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
-test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
-contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
-contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
-contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo contrib/ring/ring.cmo
-contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
-contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
-contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
-contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
-contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
-contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
-contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
-contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
-contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
-contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
-contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
-contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
-contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/ctast.cmo contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo
-contrib/interface/AddDad.vo: contrib/interface/AddDad.v
-contrib/graphs/zcgraph.vo: contrib/graphs/zcgraph.v contrib/graphs/cgraph.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Addec.vo
-contrib/graphs/cgraph.vo: contrib/graphs/cgraph.v theories/IntMap/Allmaps.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Wf_nat.vo
-contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo
-contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
-contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/field.cmo
-contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
-contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
-contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
-contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v
-contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
-contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
-contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
-contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
-contrib/correctness/Programs_stuff.vo: contrib/correctness/Programs_stuff.v contrib/correctness/Arrays_stuff.vo
-contrib/correctness/ProgramsExtraction.vo: contrib/correctness/ProgramsExtraction.v contrib/extraction/Extraction.vo contrib/correctness/Correctness.vo contrib/correctness/pextract.cmo
-contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
-contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/ZArith/ZArith.vo theories/Bool/Sumbool.vo
-contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo
-contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
-contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
-contrib/correctness/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo
-contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
-tactics/Tauto.vo: tactics/Tauto.v
-tactics/Setoid_replace.vo: tactics/Setoid_replace.v
-tactics/Refine.vo: tactics/Refine.v
-tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
-tactics/Equality.vo: tactics/Equality.v
-tactics/EqDecide.vo: tactics/EqDecide.v
-tactics/EAuto.vo: tactics/EAuto.v
-tactics/AutoRewrite.vo: tactics/AutoRewrite.v
-syntax/PPTactic.vo: syntax/PPTactic.v
-syntax/PPConstr.vo: syntax/PPConstr.v
-syntax/PPCases.vo: syntax/PPCases.v
-syntax/MakeBare.vo: syntax/MakeBare.v syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v
-states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo test-suite/success/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/EqDecide.vo contrib/extraction/Extraction.vo
+theories/Logic/JMeq.vo: theories/Logic/JMeq.v
+theories/Logic/Decidable.vo: theories/Logic/Decidable.v
+theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v theories/Logic/Elimdep.vo
+theories/Logic/Berardi.vo: theories/Logic/Berardi.v theories/Logic/Elimdep.vo
+theories/Logic/Elimdep.vo: theories/Logic/Elimdep.v
+theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
+theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
+theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
+theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
+theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
+theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
+theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
+theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
+theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
+theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo
+theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
+theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
+theories/Init/Datatypes.vo: theories/Init/Datatypes.v
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9d6455608..57058961e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -77,14 +77,6 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Node" -> <:ast< (ShowNode) >>
       | IDENT "Show"; IDENT "Script" -> <:ast< (ShowScript) >>
       | IDENT "Show"; IDENT "Existentials" -> <:ast< (ShowEx) >>
-      | IDENT "Existential"; n = numarg; ":="; c = constrarg ->
-          <:ast< (EXISTENTIAL $n $c) >>
-      | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
-        c2 = Constr.constr ->
-          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
-      | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
-        c1 = Constr.constr ->
-          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
       | IDENT "Explain"; "Proof"; l = numarg_list ->
           <:ast< (ExplainProof ($LIST $l)) >>
       | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list ->
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 09e9adbc5..ec90fc925 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -18,6 +18,7 @@ open Instantiate
 open Environ
 open Evd
 open Proof_type
+open Proof_trees
 open Logic
 open Reductionops
 open Tacmach
@@ -79,9 +80,18 @@ let applyHead n c wc =
   apprec n c (w_type_of wc c) wc
 
 let mimick_evar hdc nargs sp wc =
-  (w_Focusing_THEN sp
+  let evd = Evd.map wc.sigma sp in
+  let wc' = extract_decl sp wc in
+  let (wc'', c) = applyHead nargs hdc wc' in
+    if wc'==wc''
+    then w_Define sp c wc
+    else 
+      let wc''' = restore_decl sp evd wc'' in
+	w_Define sp c {it = wc.it ; sigma = wc'''.sigma}
+
+(*  (w_Focusing_THEN sp
      (applyHead nargs hdc)
-     (fun c wc -> w_Define sp c wc)) wc
+     (fun c wc -> w_Define sp c wc)) wc *)
 
 
 (* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
@@ -266,7 +276,10 @@ and w_resrec metas evars wc =
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
-let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc))
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unifyTerms m n gls = 
+  tclIDTAC {it = gls.it; 
+	    sigma = (get_gc (fst (w_Unify CONV m n [] (Refiner.project_with_focus gls))))}
 
 let unify m gls =
   let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 12f928e99..c88d949af 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -27,10 +27,8 @@ open Refiner
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
 
-type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a
 type w_tactic = named_context sigma -> named_context sigma
 
-
 let local_Constraints gs = refiner Change_evars gs
 
 let startWalk gls =
@@ -45,13 +43,6 @@ let startWalk gls =
              {it=gls'.it; sigma = get_gc (ids_it wc')})*)
       else error "Walking"))
 
-let walking_THEN wt rt gls =
-  let (wc,kONT) = startWalk gls in
-  let (wc',rslt) = wt wc in 
-  tclTHEN (kONT wc') (rt rslt) gls
-
-let walking wt = walking_THEN (fun wc -> (wt wc,())) (fun () -> tclIDTAC)
-
 let extract_decl sp evc =
   let evdmap = evc.sigma in
   let evd = Evd.map evdmap sp in 
@@ -71,7 +62,7 @@ let restore_decl sp evd evc =
  *
  * It is an error to cause SP to change state while we are focused on it. *)
 
-let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
+(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
                        (wc : named_context sigma) =
   let hyps  = wc.it
   and evd   = Evd.map wc.sigma sp in
@@ -82,29 +73,20 @@ let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
     wt' rslt wc
   else 
     let wc''' = restore_decl sp evd wc'' in 
-    wt' rslt {it = hyps; sigma = wc'''.sigma}
+    wt' rslt {it = hyps; sigma = wc'''.sigma} *)
       
 let w_add_sign (id,t) (wc : named_context sigma) =
   { it = Sign.add_named_decl (id,None,t) wc.it;
     sigma = wc.sigma }
 
-let ctxt_type_of evc c = 
-  type_of (Global.env_of_context evc.it) evc.sigma c
-
-let w_IDTAC wc = wc
-
-let w_Focusing sp wt = 
-  w_Focusing_THEN sp (fun wc -> (wt wc,())) (fun _ -> w_IDTAC)
-
 let w_Focus sp wc = extract_decl sp wc
 
 let w_Underlying wc = wc.sigma
 let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
-let w_type_of wc c  = ctxt_type_of wc c
+let w_type_of wc c  =
+  type_of (Global.env_of_context wc.it) wc.sigma c
 let w_env     wc    = get_env wc
 let w_hyps    wc    = named_context (get_env wc)
-let w_ORELSE wt1 wt2 wc = 
-  try wt1 wc with e when catchable_exception e -> wt2 wc
 let w_defined_const wc sp = defined_constant (w_env wc) sp
 let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
 let w_const_value wc         = constant_value (w_env wc)
@@ -123,7 +105,7 @@ let w_Define sp c wc =
   let spdecl = Evd.map (w_Underlying wc) sp in
   let cty = 
     try 
-      ctxt_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
+      w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
     with Not_found -> 
       error "Instantiation contains unlegal variables"
   in 
@@ -141,23 +123,42 @@ let w_Define sp c wc =
 (* Instantiation of existential variables *)
 (******************************************)
 
-let instantiate_pf n c pfts = 
-  let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
-  let sigma  = (w_Underlying wc) in 
-  let (sp,_) = 
-    try 
-      List.nth (Evd.non_instantiated sigma) (n-1)
-    with Failure _ -> 
-      error "not so many uninstantiated existential variables"
+(* The instantiate tactic *)
+
+let evars_of evc c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | _ -> fold_constr evrec acc c
   in 
-  let wc' = w_Define sp c wc in 
-  let newgc = w_Underlying wc' in 
-  change_constraints_pftreestate newgc pfts
+  evrec [] c
+
+let instantiate n c gl = 
+  let wc = Refiner.project_with_focus gl in
+  let evl = evars_of wc.sigma gl.it.evar_concl in
+    if List.length evl < n then error "not enough evars";
+    let (n,_) as k = destEvar (List.nth evl (n-1)) in 
+      if Evd.is_defined wc.sigma n then 
+	error "Instantiate called on already-defined evar";
+      let wc' = w_Define n c wc in 
+	tclIDTAC {it = gl.it ; sigma = wc'.sigma}
+
+let pfic gls c =
+  let evc = gls.sigma in 
+  Astterm.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+
+let instantiate_tac = function
+  | [Integer n; Command com] ->
+      (fun gl -> instantiate n (pfic gl com) gl)
+  | [Integer n; Constr c] ->
+      (fun gl -> instantiate n c gl)
+  | _ -> invalid_arg "Instantiate called with bad arguments"
+
+(* vernac command existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
+  let wc = project_with_focus gls in
   let sigma = (w_Underlying wc) in 
   let (sp,evd) = 
     try
@@ -167,5 +168,7 @@ let instantiate_pf_com n com pfts =
   in 
   let c = Astterm.interp_constr sigma (Evarutil.evar_env evd) com in     
   let wc' = w_Define sp c wc in
-  let newgc = w_Underlying wc' in
+  let newgc = (w_Underlying wc') in
   change_constraints_pftreestate newgc pfts
+
+
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 9f09cfba5..4138a49c3 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -32,7 +32,6 @@ val rc_of_glsigma : goal sigma -> named_context sigma
     hyps  : context of the goal;
     decls : a superset of evars of which the goal may depend })]
 *)
-type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a
 
 (* A [w_tactic] is a tactic which modifies the a set of evars of which
 a goal depend, either by instantiating one, or by declaring a new
@@ -45,10 +44,12 @@ val local_Constraints :
 val startWalk : 
   goal sigma -> named_context sigma * (named_context sigma -> tactic)
 
-val walking_THEN    : 'a result_w_tactic -> ('a -> tactic) -> tactic
-val walking         : w_tactic -> tactic
-val w_Focusing_THEN : 
-  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
+val extract_decl : evar -> named_context sigma -> named_context sigma
+
+val restore_decl : evar -> evar_info -> named_context sigma -> named_context sigma
+
+(* val w_Focusing_THEN : 
+  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic *)
 
 val w_Declare    : evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
@@ -61,9 +62,6 @@ val w_type_of    : named_context sigma -> constr -> constr
 val w_add_sign   : (identifier * types) -> named_context sigma 
                      -> named_context sigma
 
-val w_IDTAC      : w_tactic
-val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
-val ctxt_type_of : named_context sigma -> constr -> constr
 val w_whd_betadeltaiota : named_context sigma -> constr -> constr
 val w_hnf_constr        : named_context sigma -> constr -> constr
 val w_conv_x            : named_context sigma -> constr -> constr -> bool
@@ -71,5 +69,6 @@ val w_const_value       : named_context sigma -> constant -> constr
 val w_defined_const     : named_context sigma -> constant -> bool
 val w_defined_evar      : named_context sigma -> existential_key -> bool
 
-val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate : evar -> constr -> tactic
+val instantiate_tac : tactic_arg list -> tactic
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f6424df8d..2b8416eae 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -223,7 +223,7 @@ let solve_nth k tac =
 let by tac = mutate (solve_pftreestate tac)
 
 let instantiate_nth_evar_com n c =
-  mutate (instantiate_pf_com n c)
+  mutate (Evar_refiner.instantiate_pf_com n c)
 
 let traverse n = mutate (traverse n)
  
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5e4b6b495..03f3d906c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -163,8 +163,6 @@ let prev_unproven           = prev_unproven
 let top_of_tree             = top_of_tree
 let frontier                = frontier
 let change_constraints_pftreestate = change_constraints_pftreestate
-let instantiate_pf     = Evar_refiner.instantiate_pf
-let instantiate_pf_com = Evar_refiner.instantiate_pf_com
 
 (*************************************************)
 (* Tacticals re-exported from the Refiner module.*)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 0a685a447..7dda94210 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -89,7 +89,7 @@ val frontier : transformation_tactic
 
 (*s Functions for handling the state of the proof editor. *)
 
-type pftreestate
+type pftreestate = Refiner.pftreestate
 
 val proof_of_pftreestate    : pftreestate -> proof_tree
 val cursor_of_pftreestate   : pftreestate -> int list
@@ -114,9 +114,6 @@ val prev_unproven           : pftreestate -> pftreestate
 val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
-val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
-val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
-
 
 (*s Tacticals re-exported from the Refiner module. *)
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3928d6a5e..01e7cca46 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -79,36 +79,6 @@ let prolog_tac l n gl =
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
 
-let evars_of evc c = 
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
-    | _ -> fold_constr evrec acc c
-  in 
-  evrec [] c
-
-let instantiate n c gl =
-  let sigma = project gl in
-  let evl = evars_of sigma (pf_concl gl) in
-  let (wc,kONT) = startWalk gl in
-  if List.length evl < n then error "not enough evars";
-  let (n,_) as k = destEvar (List.nth evl (n-1)) in 
-  if Evd.is_defined sigma n then 
-    error "Instantiate called on already-defined evar";
-  let wc' = w_Define n c wc in 
-  kONT wc' gl
-
-let instantiate_tac = function
-  | [Integer n; Command com] ->
-      (fun gl -> instantiate n (pf_interp_constr gl com) gl)
-  | [Integer n; Constr c] ->
-      (fun gl -> instantiate n c gl)
-  | _ -> invalid_arg "Instantiate called with bad arguments"
-
-let normEvars gl =
-  let sigma = project gl in
-  convert_concl (nf_betaiota (Evarutil.nf_evar sigma (pf_concl gl))) gl
-
 let vernac_prolog =
   let uncom = function
     | Constr c -> c
@@ -123,12 +93,6 @@ let vernac_prolog =
   fun coms n -> 
     gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
 
-let vernac_instantiate =
-  hide_tactic "Instantiate" instantiate_tac
-
-let vernac_normevars =
-  hide_atomic_tactic "NormEvars" normEvars
-
 open Auto
 
 (***************************************************************************)
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index b44054660..d7397e8fc 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -52,4 +52,6 @@ let v_destruct      = hide_tactic "Destruct"      dyn_destruct
 let v_new_destruct  = hide_tactic "NewDestruct"   dyn_new_destruct
 let v_fix           = hide_tactic "Fix"           dyn_mutual_fix
 let v_cofix         = hide_tactic "Cofix"         dyn_mutual_cofix
+let vernac_instantiate =
+  hide_tactic "Instantiate" Evar_refiner.instantiate_tac
 
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index cb5cf8385..86ab39dff 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -52,3 +52,4 @@ val v_destruct      : tactic_arg list -> tactic
 (*i val v_new_destruct  : tactic_arg list -> tactic i*)
 val v_fix           : tactic_arg list -> tactic
 val v_cofix         : tactic_arg list -> tactic
+val vernac_instantiate : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c9247c09e..e7d61a79a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1868,3 +1868,6 @@ let dyn_tclABSTRACT =
        | [Identifier s; Tac (tac,_)] ->
 	   tclABSTRACT (Some s) tac
        | _ -> invalid_arg "tclABSTRACT") 
+
+
+
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 3b93cce07..a8d53dae9 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -99,30 +99,8 @@ let clenv_constrain_with_bindings bl clause =
     in 
     matchrec clause bl
 
-let add_prod_rel sigma (t,env) =
-  match kind_of_term t with
-    | Prod (na,t1,b) ->
-        (b,push_rel_assum (na, t1) env)
-    | LetIn (na,c1,t1,b) ->
-        (b,push_rel (na,Some c1, t1) env)
-    | _ -> failwith "add_prod_rel"
-
-let rec add_prods_rel sigma (t,env) =
-  try 
-    add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota env sigma t,env))
-  with Failure "add_prod_rel" -> 
-    (t,env)
-
 (* What follows is part of the contents of the former file tactics3.ml *)
     
-let res_pf_THEN kONT clenv tac gls =
-  let clenv' = (clenv_unique_resolver false clenv gls) in 
-  (tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
-
-let res_pf_THEN_i kONT clenv tac gls =
-  let clenv' = (clenv_unique_resolver false clenv gls) in 
-  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
-
 let elim_res_pf_THEN_i kONT clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
   tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
@@ -185,21 +163,3 @@ let applyUsing c gl =
   let clause = mk_clenv_using wc c in 
   res_pf kONT clause gl
 
-let clenv_apply_n_times n ce =
-  let templtyp = clenv_instance_template_type ce
-  and templval = (clenv_template ce).rebus in   
-  let rec apprec ce argacc (n,ty) =
-    let env = Global.env () in
-    let templtyp = whd_betadeltaiota env (w_Underlying ce.hook) ty in
-    match (n, kind_of_term templtyp) with 
-      | (0, _) ->
-	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
-      | (n, Prod (na,dom,rng)) ->
-          let mv = new_meta() in
-          let newce = clenv_pose (na,mv,dom) ce in
-	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
-      | (n, LetIn (na,b,t,c)) ->
-	  apprec ce argacc (n, subst1 b c)
-      | (n, _) -> failwith "clenv_apply_n_times"
-  in 
-  apprec ce [] (n, templtyp)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 24174e508..26c46e89a 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -36,9 +36,6 @@ type wc = named_context sigma
 
 val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
-val add_prod_rel : evar_map -> constr * env -> constr * env
-val add_prods_rel : evar_map -> constr * env -> constr * env
-
 (*i**
 val add_prod_sign : 
   'a evar_map -> constr * types signature -> constr * types signature
@@ -47,22 +44,7 @@ val add_prods_sign :
   'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
-val res_pf_THEN : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
-
-(* This behaves as [res_pf_THEN] but the tactic applied then takes
-   also the subgoal number (starting from 1) as argument *)
-val res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
-
 val elim_res_pf_THEN_i : 
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
 
-val mk_clenv_using : wc -> constr -> wc clausenv
-
 val applyUsing : constr -> tactic
-
-val clenv_apply_n_times : int -> wc clausenv -> wc clausenv
-
-
-
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6fd7f8858..52bd586ca 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -22,6 +22,7 @@ open Pfedit
 open Tacmach
 open Proof_trees
 open Proof_type
+open Evar_refiner
 open Tacred
 open Environ
 open Vernacinterp