Ground update, new files.

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

11 files changed, 405 insertions, 318 deletions

diff --git a/.depend b/.depend
index 371e2ea23..a577408e7 100644
--- a/.depend
+++ b/.depend
@@ -45,10 +45,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi 
 kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -68,9 +68,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/bignat.cmi: lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -99,6 +96,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
 library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
     lib/util.cmi 
@@ -244,8 +244,8 @@ tactics/contradiction.cmi: kernel/names.cmi proofs/proof_type.cmi \
 tactics/dhyp.cmi: kernel/names.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     interp/topconstr.cmi 
 tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
-    tactics/tacticals.cmi kernel/term.cmi 
+    pretyping/rawterm.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    kernel/term.cmi 
 tactics/equality.cmi: kernel/environ.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
     proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
@@ -318,11 +318,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
     kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -340,11 +340,11 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -406,14 +406,16 @@ contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
 contrib/first-order/formula.cmi: library/libnames.cmi kernel/names.cmi \
     proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
-contrib/first-order/rules.cmi: contrib/first-order/formula.cmi \
-    library/libnames.cmi kernel/names.cmi contrib/first-order/sequent.cmi \
-    proofs/tacmach.cmi kernel/term.cmi contrib/first-order/unify.cmi 
+contrib/first-order/instances.cmi: contrib/first-order/formula.cmi \
+    library/libnames.cmi kernel/names.cmi contrib/first-order/rules.cmi \
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
+    contrib/first-order/unify.cmi 
+contrib/first-order/rules.cmi: library/libnames.cmi kernel/names.cmi \
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi 
 contrib/first-order/sequent.cmi: contrib/first-order/formula.cmi lib/heap.cmi \
     library/libnames.cmi kernel/names.cmi proofs/proof_type.cmi \
     proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
-contrib/first-order/unify.cmi: contrib/first-order/formula.cmi \
-    library/libnames.cmi contrib/first-order/sequent.cmi kernel/term.cmi 
+contrib/first-order/unify.cmi: kernel/term.cmi 
 contrib/funind/tacinvutils.cmi: interp/coqlib.cmi tactics/equality.cmi \
     pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \
     parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
@@ -487,12 +489,20 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
 ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx 
 ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi 
 ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi 
+ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
-    ide/ideutils.cmi library/lib.cmi library/libnames.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    ide/ideutils.cmi library/lib.cmi library/libnames.cmi toplevel/mltop.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \
+    proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
     pretyping/reductionops.cmi proofs/refiner.cmi library/states.cmi \
     tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tactics.cmi \
     kernel/term.cmi lib/util.cmi toplevel/vernac.cmi \
@@ -500,23 +510,15 @@ ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
 ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     kernel/declarations.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \
-    ide/ideutils.cmx library/lib.cmx library/libnames.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    ide/ideutils.cmx library/lib.cmx library/libnames.cmx toplevel/mltop.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
+    proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx library/states.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
-    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
-    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
-    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
-    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -667,6 +669,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -675,12 +683,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
     lib/predicate.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -761,10 +763,10 @@ 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 
@@ -773,24 +775,14 @@ lib/heap.cmo: lib/heap.cmi
 lib/heap.cmx: lib/heap.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -895,6 +887,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -2019,10 +2021,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
     tactics/wcclausenv.cmi 
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -2229,18 +2231,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
-    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
-    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
-    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
-    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2301,6 +2291,18 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
     proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
+    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
+    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2377,6 +2379,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2393,18 +2407,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2789,54 +2791,64 @@ contrib/first-order/formula.cmx: interp/coqlib.cmx kernel/declarations.cmx \
     contrib/first-order/formula.cmi 
 contrib/first-order/ground.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
     contrib/first-order/formula.cmi interp/genarg.cmi library/goptions.cmi \
-    library/libnames.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
-    proofs/proof_trees.cmi proofs/refiner.cmi contrib/first-order/rules.cmi \
-    contrib/first-order/sequent.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
-    proofs/tacmach.cmi proofs/tactic_debug.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi contrib/first-order/unify.cmi \
-    lib/util.cmi 
+    contrib/first-order/instances.cmi library/libnames.cmi parsing/pcoq.cmi \
+    lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi proofs/refiner.cmi \
+    contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
+    proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \
+    proofs/tactic_debug.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
 contrib/first-order/ground.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     contrib/first-order/formula.cmx interp/genarg.cmx library/goptions.cmx \
-    library/libnames.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
-    proofs/proof_trees.cmx proofs/refiner.cmx contrib/first-order/rules.cmx \
-    contrib/first-order/sequent.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
-    proofs/tacmach.cmx proofs/tactic_debug.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx contrib/first-order/unify.cmx \
-    lib/util.cmx 
-contrib/first-order/rules.cmo: interp/coqlib.cmi kernel/declarations.cmi \
-    contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
+    contrib/first-order/instances.cmx library/libnames.cmx parsing/pcoq.cmx \
+    lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx proofs/refiner.cmx \
+    contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
+    proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
+    proofs/tactic_debug.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx 
+contrib/first-order/instances.cmo: kernel/declarations.cmi \
+    contrib/first-order/formula.cmi library/libnames.cmi \
     pretyping/rawterm.cmi pretyping/reductionops.cmi \
-    contrib/first-order/sequent.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
     proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
     kernel/term.cmi pretyping/termops.cmi contrib/first-order/unify.cmi \
-    lib/util.cmi contrib/first-order/rules.cmi 
-contrib/first-order/rules.cmx: interp/coqlib.cmx kernel/declarations.cmx \
-    contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
+    lib/util.cmi contrib/first-order/instances.cmi 
+contrib/first-order/instances.cmx: kernel/declarations.cmx \
+    contrib/first-order/formula.cmx library/libnames.cmx \
     pretyping/rawterm.cmx pretyping/reductionops.cmx \
-    contrib/first-order/sequent.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx pretyping/termops.cmx contrib/first-order/unify.cmx \
-    lib/util.cmx contrib/first-order/rules.cmi 
+    lib/util.cmx contrib/first-order/instances.cmi 
+contrib/first-order/rules.cmo: interp/coqlib.cmi kernel/declarations.cmi \
+    contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
+    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
+    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/first-order/rules.cmi 
+contrib/first-order/rules.cmx: interp/coqlib.cmx kernel/declarations.cmx \
+    contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
+    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
+    kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/first-order/rules.cmi 
 contrib/first-order/sequent.cmo: tactics/auto.cmi interp/constrextern.cmi \
     contrib/first-order/formula.cmi library/global.cmi lib/heap.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi parsing/ppconstr.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
-    contrib/first-order/sequent.cmi 
+    proofs/tacmach.cmi kernel/term.cmi contrib/first-order/unify.cmi \
+    lib/util.cmi contrib/first-order/sequent.cmi 
 contrib/first-order/sequent.cmx: tactics/auto.cmx interp/constrextern.cmx \
     contrib/first-order/formula.cmx library/global.cmx lib/heap.cmx \
     library/libnames.cmx kernel/names.cmx lib/pp.cmx parsing/ppconstr.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
-    contrib/first-order/sequent.cmi 
-contrib/first-order/unify.cmo: proofs/clenv.cmi \
-    contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
-    pretyping/pattern.cmi pretyping/reductionops.cmi \
-    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi contrib/first-order/unify.cmi 
-contrib/first-order/unify.cmx: proofs/clenv.cmx \
-    contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
-    pretyping/pattern.cmx pretyping/reductionops.cmx \
-    contrib/first-order/sequent.cmx proofs/tacmach.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx contrib/first-order/unify.cmi 
+    proofs/tacmach.cmx kernel/term.cmx contrib/first-order/unify.cmx \
+    lib/util.cmx contrib/first-order/sequent.cmi 
+contrib/first-order/unify.cmo: contrib/first-order/formula.cmi \
+    kernel/names.cmi pretyping/reductionops.cmi proofs/tacmach.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    contrib/first-order/unify.cmi 
+contrib/first-order/unify.cmx: contrib/first-order/formula.cmx \
+    kernel/names.cmx pretyping/reductionops.cmx proofs/tacmach.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    contrib/first-order/unify.cmi 
 contrib/fourier/fourierR.cmo: proofs/clenv.cmi tactics/contradiction.cmi \
     interp/coqlib.cmi tactics/equality.cmi contrib/fourier/fourier.cmo \
     library/libnames.cmi library/library.cmi kernel/names.cmi \
@@ -3057,6 +3069,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
     contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
     parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -3081,14 +3101,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -3319,12 +3331,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
     kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi 
 contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
     kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx 
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
     library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -3379,8 +3391,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
     contrib/xml/xml.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
     contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -3405,10 +3415,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
 contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
-    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
-    ide/utils/configwin_types.cmx ide/utils/configwin.cmi 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
     ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
     ide/utils/uoptions.cmi 
@@ -3419,6 +3427,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
     ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi 
 ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
     ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx 
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+    ide/utils/configwin_types.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
     ide/utils/uoptions.cmi 
 ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/Makefile b/Makefile
index 847a1eac9..b0d35951b 100644
--- a/Makefile
+++ b/Makefile
@@ -279,7 +279,7 @@ FUNINDCMO=\
 FOCMO=\
   contrib/first-order/formula.cmo contrib/first-order/sequent.cmo \
   contrib/first-order/unify.cmo contrib/first-order/rules.cmo \
-  contrib/first-order/ground.cmo
+  contrib/first-order/instances.cmo contrib/first-order/ground.cmo
 
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index f0cd3afa6..b8f684977 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -13,6 +13,7 @@
 open Formula
 open Sequent
 open Rules
+open Instances
 open Term
 open Tacmach
 open Tactics
@@ -79,7 +80,8 @@ let ground_tac solver startseq gl=
 		       cont_tac gl
 		     else 
 		       (match 
-			  Unify.give_right_instances i dom triv atoms seq with
+			  Instances.give_right_instances i dom triv atoms seq 
+			with
 			      Some l -> tclORELSE
 				(exists_tac l toptac (re_add seq)) cont_tac gl
 			    | None ->
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
new file mode 100644
index 000000000..8625c988d
--- /dev/null
+++ b/contrib/first-order/instances.ml
@@ -0,0 +1,178 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Formula
+open Sequent
+open Unify
+open Rules
+open Util
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Termops
+open Reductionops
+open Declarations
+open Formula
+open Sequent
+open Libnames
+
+let rev_rels n t= (* requires n = max (free_rels t) *) 
+  let l=list_tabulate (fun i->mkRel (n-i)) n in
+    substl l t
+ 	  
+let renum_metas_from k n t=(* requires n = max (free_rels t) *)
+  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+    substl l t
+
+(* ordre lexico:
+   nombre de metas dans terme;
+   profondeur de matching;
+   le reste
+*)
+      
+let compare_instance inst1 inst2=
+	match inst1,inst2 with
+	    Phantom(d1),Phantom(d2)->
+	      (OrderedConstr.compare d1 d2)
+	  | Real((m1,c1),n1),Real((m2,c2),n2)->
+	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n2 n1 c1 c2
+	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
+	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
+
+module OrderedRightInstance=
+struct 
+  type t = instance
+  let compare = compare_instance
+end
+
+module OrderedLeftInstance=
+struct
+  type t=instance * Libnames.global_reference
+  let compare (inst1,id1) (inst2,id2)=
+    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
+    (* we want a __decreasing__ total order *)
+end
+  
+module RIS=Set.Make(OrderedRightInstance)
+module LIS=Set.Make(OrderedLeftInstance)
+
+let make_goal_atoms seq=
+  match seq.gl with
+      Atomic t->{negative=[];positive=[t]}
+    | Complex (_,_,l)->l 
+
+let make_left_atoms seq=
+    {negative=seq.latoms;positive=[]}
+
+let do_sequent setref triv add mkelt seq i dom atoms=
+  let flag=ref true in
+  let phref=ref triv in
+  let do_atoms a1 a2 =
+    let do_pair t1 t2 = 
+      match unif_atoms i dom t1 t2 with
+	  None->()
+	| Some (Phantom _) ->phref:=true
+	| Some c ->flag:=false;setref:=add (mkelt c) !setref in
+      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
+      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
+    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
+    do_atoms atoms (make_left_atoms seq);
+    do_atoms atoms (make_goal_atoms seq);
+    !flag && !phref 
+ 
+let give_right_instances i dom triv atoms seq=
+  let setref=ref RIS.empty in
+  let inj inst=inst in
+  if do_sequent setref triv RIS.add inj seq i dom atoms then
+    None
+  else
+    Some (RIS.elements !setref)
+
+let match_one_forall_hyp setref seq lf=
+  match lf.pat with 
+      Lforall(i,dom,triv)->
+	let inj x=(x,lf.id) in
+	  if do_sequent setref triv LIS.add inj seq i dom lf.atoms then
+	    setref:=LIS.add ((Phantom dom),lf.id) !setref 
+    | _ ->anomaly "can't happen" 
+
+let give_left_instances lfh seq=
+  let setref=ref LIS.empty in
+    List.iter (match_one_forall_hyp setref seq) lfh;
+    LIS.elements !setref
+	  	  
+(*tactics*)
+
+
+let rec collect_forall seq=
+  if is_empty_left seq then ([],seq) 
+  else
+    let hd,seq1=take_left seq in
+      (match hd.pat with 
+	   Lforall(_,_,_)-> 
+	     let (q,seq2)=collect_forall seq1 in
+	       ((hd::q),seq2)
+	 | _->[],seq)
+
+let left_instance_tac (inst,id) tacrec seq=
+  match inst with
+      Phantom dom->
+	if lookup (id,None) seq then 
+	  tclFAIL 0 "already done"
+	else
+	  tclTHENS (cut dom) 
+	    [tclTHENLIST
+	       [intro;
+		(fun gls->generalize 
+		   [mkApp(constr_of_reference id,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+		intro;
+		tclSOLVE [wrap 1 false tacrec 
+			    (deepen (record (id,None) seq))]];
+	    tclTRY assumption]
+    | Real((m,t) as c,_)->
+	if lookup (id,Some c) seq || m>0 then 
+	  tclFAIL 0 "already done" 
+	else
+	  tclTHENLIST 
+	    [generalize [mkApp(constr_of_reference id,[|t|])];
+	     intro; 
+	     tclSOLVE 
+	       [wrap 1 false tacrec 
+		  (deepen (record (id,Some c) seq))]]
+
+let left_forall_tac lfp tacrec seq gl=
+  let insts=give_left_instances lfp seq in
+    tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl
+	  
+let dummy_exists_tac dom  tacrec seq=
+	tclTHENS (cut dom) 
+	[tclTHENLIST
+	   [intro;
+	    (fun gls->
+	       split (Rawterm.ImplicitBindings 
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
+	 tclTRY assumption] 
+ 
+let right_instance_tac inst tacrec seq=
+  match inst with
+      Phantom _ ->anomaly "can't happen" 
+    | Real ((m,t),_) ->
+	if m>0 then tclFAIL 0 "not implemented ... yes"
+	else
+	tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclSOLVE [wrap 0 true tacrec (deepen seq)])
+
+let exists_tac insts tacrec seq gl=
+    tclFIRST 
+      (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
+
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
new file mode 100644
index 000000000..b1d88280b
--- /dev/null
+++ b/contrib/first-order/instances.mli
@@ -0,0 +1,40 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Term
+open Tacmach
+open Names
+open Libnames
+open Rules
+  
+val give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> 
+  Sequent.t -> Unify.instance list option
+
+val give_left_instances : Formula.left_formula list-> Sequent.t -> 
+  (Unify.instance*global_reference) list
+
+val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t
+
+val left_instance_tac : Unify.instance * global_reference -> seqtac
+
+val left_forall_tac : Formula.left_formula list -> seqtac
+
+val dummy_exists_tac : constr -> seqtac
+
+val right_instance_tac : Unify.instance -> seqtac
+
+val exists_tac : Unify.instance list -> seqtac
+	       
+
+
+
+
+
+
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 01ae688ad..c5c7319e8 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -19,7 +19,6 @@ open Reductionops
 open Declarations
 open Formula
 open Sequent
-open Unify
 open Libnames
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
@@ -193,64 +192,7 @@ let ll_forall_tac prod id tacrec seq=
 
 (* complicated stuff for instantiation with unification *)
 
-let rec collect_forall seq=
-  if is_empty_left seq then ([],seq) 
-  else
-    let hd,seq1=take_left seq in
-      (match hd.pat with 
-	   Lforall(_,_,_)-> 
-	     let (q,seq2)=collect_forall seq1 in
-	       ((hd::q),seq2)
-	 | _->[],seq)
-
-let left_instance_tac (inst,id) tacrec seq=
-  match inst with
-      Phantom dom->
-	if lookup id None seq then 
-	  tclFAIL 0 "already done"
-	else
-	  tclTHENS (cut dom) 
-	    [tclTHENLIST
-	       [intro;
-		(fun gls->generalize 
-		   [mkApp(constr_of_reference id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		intro;
-		tclSOLVE [wrap 1 false tacrec 
-			    (deepen (record id None seq))]];
-	    tclTRY assumption]
-    | Real(t,_)->
-	if lookup id (Some t) seq then 
-	  tclFAIL 0 "already done" 
-	else
-	  tclTHENLIST 
-	    [generalize [mkApp(constr_of_reference id,[|t|])];
-	     intro; 
-	     tclSOLVE 
-	       [wrap 1 false tacrec 
-		  (deepen (record id (Some t) seq))]]
-
-let left_forall_tac lfp tacrec seq gl=
-  let insts=give_left_instances lfp seq in
-    tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl
-	  
-let dummy_exists_tac dom  tacrec seq=
-	tclTHENS (cut dom) 
-	[tclTHENLIST
-	   [intro;
-	    (fun gls->
-	       split (Rawterm.ImplicitBindings 
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
-	    tclSOLVE [wrap 0 false tacrec (deepen seq)]];
-	 tclTRY assumption] 
- 
-let right_instance_tac (t,_) tacrec seq=
-	tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	(tclSOLVE [wrap 0 true tacrec (deepen seq)])
-
-let exists_tac insts tacrec seq gl=
-    tclFIRST 
-      (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl
+(* moved to instances.ml *)
 
 (* special for compatibility with old Intuition *)
 
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 045316263..10ffe863d 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -19,47 +19,37 @@ type lseqtac= global_reference -> seqtac
 
 val wrap : int -> bool -> seqtac
 
+val id_of_global: global_reference -> identifier
+
 val clear_global: global_reference -> tactic
 
 val axiom_tac : constr -> Sequent.t -> tactic
 
+val ll_atom_tac : constr -> lseqtac
+
 val evaluable_tac : evaluable_global_reference -> seqtac
 
 val left_evaluable_tac : evaluable_global_reference -> lseqtac
 
 val and_tac : seqtac
 
-val left_and_tac : inductive -> lseqtac
-
 val or_tac : seqtac
 
-val left_or_tac : inductive -> lseqtac
-
-val forall_tac : seqtac
-
-val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t
-
-val left_instance_tac : Unify.instance * global_reference -> seqtac
-
-val left_forall_tac : Formula.left_formula list -> seqtac
-
 val arrow_tac : seqtac
 
-val dummy_exists_tac : constr -> seqtac
+val left_and_tac : inductive -> lseqtac
 
-val right_instance_tac : constr * int -> seqtac
+val left_or_tac : inductive -> lseqtac
 
-val exists_tac : (constr * int) list -> seqtac
-	       
-val left_exists_tac : inductive -> lseqtac
+val left_false_tac : global_reference -> tactic
 
-val ll_arrow_tac : constr -> constr -> constr -> lseqtac
+val ll_ind_tac : inductive -> constr list -> lseqtac
 
-val ll_atom_tac : constr -> lseqtac
+val ll_arrow_tac : constr -> constr -> constr -> lseqtac
 
-val left_false_tac : global_reference -> tactic
+val forall_tac : seqtac
 
-val ll_ind_tac : inductive -> constr list -> lseqtac
+val left_exists_tac : inductive -> lseqtac
 
 val ll_forall_tac : types -> lseqtac
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4ece7c8c5..91a8f1ddd 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -11,6 +11,7 @@
 open Term
 open Util
 open Formula
+open Unify
 open Tacmach
 open Names
 open Libnames
@@ -120,14 +121,17 @@ struct
   let compare=compare_constr
 end
 
+type h_item = global_reference * (int*constr) option
+
 module Hitem=
 struct 
-  type t=(global_reference * constr option)
+  type t = h_item
   let compare (id1,co1) (id2,co2)=
     (Pervasives.compare 
      =? (fun oc1 oc2 ->
 	   match oc1,oc2 with 
-	       Some c1,Some c2 -> OrderedConstr.compare c1 c2
+	       Some (m1,c1),Some (m2,c2) -> 
+		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
 	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
 end
 
@@ -163,9 +167,9 @@ type t=
 
 let deepen seq={seq with depth=seq.depth-1}
  
-let record id topt seq={seq with history=History.add (id,topt) seq.history}
+let record item seq={seq with history=History.add item seq.history}
 
-let lookup id topt seq=History.mem (id,topt) seq.history
+let lookup item seq=History.mem item seq.history
 
 let add_left (nam,t) seq internal gl=
   match build_left_entry nam t internal gl seq.cnt with
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 851396d45..79cf0d1ed 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -23,7 +23,9 @@ module OrderedConstr: Set.OrderedType with type t=constr
 
 module CM: Map.S with type key=constr
 
-module History: Set.S with type elt = global_reference * constr option
+type h_item = global_reference * (int*constr) option
+
+module History: Set.S with type elt = h_item
 
 val cm_add : constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
@@ -43,9 +45,9 @@ type t = {redexes:HP.t;
 
 val deepen: t -> t
 
-val record: global_reference -> constr option -> t -> t
+val record: h_item -> t -> t
 
-val lookup: global_reference -> constr option -> t -> bool
+val lookup: h_item -> t -> bool
 
 val add_left : global_reference * constr -> t -> bool -> 
   Proof_type.goal sigma -> t
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index b9c3a1a42..30ff1c811 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -10,17 +10,22 @@
 
 open Util
 open Formula 
-open Sequent
 open Tacmach
 open Term
 open Names
 open Termops
-open Pattern
 open Reductionops
 
 exception UFAIL of constr*constr
 
-let unif t1 t2= (* Martelli-Montanari style *)
+(* 
+   RIGID-only Martelli-Montanari style unification for CLOSED terms 
+   I repeat : t1 and t2 must NOT have ANY free deBruijn                        
+   sigma is kept normal with respect to itself but is lazily applied 
+   to the equation set. Raises UFAIL with a pair of  terms 
+*)
+
+let unif t1 t2= 
   let bige=Queue.create () 
   and sigma=ref [] in
   let bind i t=
@@ -83,9 +88,6 @@ let unif t1 t2= (* Martelli-Montanari style *)
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
-(* collect tries finds ground instantiations for Meta i*)
-let is_ground t=(Clenv.collect_metas t)=[]
-
 let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
 
 let value i t=
@@ -100,7 +102,7 @@ let value i t=
     vaux t
 	  
 type instance=
-    Real of (constr*int) (* instance*valeur heuristique*)
+    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr (* domaine de quantification *)
 
 let mk_rel_inst t=
@@ -118,97 +120,15 @@ let mk_rel_inst t=
 	       mkRel (m+d))
       | _ -> map_constr_with_binders succ renum_rec d t
   in 
-  let nt=renum_rec 0 t in
-    (!new_rel - 1,nt)
- 	  
+  let nt=renum_rec 0 t in (!new_rel - 1,nt)
+
 let unif_atoms i dom t1 t2=
-  if is_head_meta t1 || is_head_meta t2  then None else
+  if is_head_meta t1 || is_head_meta t2 then None else
     try 
       let t=List.assoc i (unif t1 t2) in 
-	if is_ground t then Some (Real(t,value i t1))
-	else if is_head_meta t then Some (Phantom dom)
-	else None
+	if is_head_meta t then Some (Phantom dom)
+	else Some (Real(mk_rel_inst t,value i t1))
     with
 	UFAIL(_,_) ->None
       | Not_found ->Some (Phantom dom)
-
-(* ordre lexico:
-   nombre de metas dans terme;
-   profondeur de matching;
-   le reste
-*)
-
-      
-let compare_instance inst1 inst2=
-	match inst1,inst2 with
-	    Phantom(d1),Phantom(d2)->
-	      (OrderedConstr.compare d1 d2)
-	  | Real(c1,n1),Real(c2,n2)->
-	      ((-) =? OrderedConstr.compare) n2 n1 c1 c2
-	  | Phantom(_),_-> 1
-	  | _,_-> -1
-
-module OrderedRightInstance=
-struct 
-  type t = constr*int
-  let compare (c1,n1) (c2,n2) = ((-) =? OrderedConstr.compare) n2 n1 c1 c2
-end
-
-module OrderedLeftInstance=
-struct
-  type t=instance * Libnames.global_reference
-  let compare (inst1,id1) (inst2,id2)=
-    (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2
-    (* we want a __decreasing__ total order *)
-end
-  
-module RIS=Set.Make(OrderedRightInstance)
-module LIS=Set.Make(OrderedLeftInstance)
-
-let make_goal_atoms seq=
-  match seq.gl with
-      Atomic t->{negative=[];positive=[t]}
-    | Complex (_,_,l)->l 
-
-let make_left_atoms seq=
-    {negative=seq.latoms;positive=[]}
-
-let do_sequent setref triv add mkelt seq i dom atoms=
-  let flag=ref true in
-  let phref=ref triv in
-  let do_atoms a1 a2 =
-    let do_pair t1 t2 = 
-      match unif_atoms i dom t1 t2 with
-	  None->()
-	| Some (Phantom _) ->phref:=true
-	| Some c ->flag:=false;setref:=add (mkelt c) !setref in
-      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
-      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
-    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
-    do_atoms atoms (make_left_atoms seq);
-    do_atoms atoms (make_goal_atoms seq);
-    !flag && !phref 
- 
-let give_right_instances i dom triv atoms seq=
-  let setref=ref RIS.empty in
-  let inj=function
-       Real c->c
-     | _->anomaly "can't happen" in
-  if do_sequent setref triv RIS.add inj seq i dom atoms then
-    None
-  else
-    Some (RIS.elements !setref)
-
-let match_one_forall_hyp setref seq lf=
-  match lf.pat with 
-      Lforall(i,dom,triv)->
-	let inj x=(x,lf.id) in
-	  if do_sequent setref triv LIS.add inj seq i dom lf.atoms then
-	    setref:=LIS.add ((Phantom dom),lf.id) !setref 
-    | _ ->anomaly "can't happen" 
-
-let give_left_instances lfh seq=
-  let setref=ref LIS.empty in
-    List.iter (match_one_forall_hyp setref seq) lfh;
-    LIS.elements !setref
-
+	  
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 7effac207..013fc73cd 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -8,17 +8,14 @@
 
 (* $Id$ *)
 
-open Libnames
 open Term
 
+exception UFAIL of constr*constr
+
+val unif : constr -> constr -> (int*constr) list
+
 type instance=
-    Real of (constr*int) (* instance*valeur heuristique*)
-  | Phantom of constr (* domaine de quantification *)
+    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
+  | Phantom of constr        (* domaine de quantification *)
 
 val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
-  
-val give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> 
-  Sequent.t -> (constr*int) list option
-
-val give_left_instances : Formula.left_formula list-> Sequent.t -> 
-  (instance*global_reference) list