Major Ground tactic update, sensible performance improvement

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

10 files changed, 424 insertions, 223 deletions

diff --git a/.depend b/.depend
index 25e6e0022d..1e23c26f42 100644
--- a/.depend
+++ b/.depend
@@ -43,10 +43,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 
@@ -66,9 +66,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 \
@@ -97,6 +94,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
 library/nameops.cmi: kernel/names.cmi lib/pp.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 
@@ -315,11 +315,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 parsing/pcoq.cmi lib/pp.cmi interp/ppextend.cmi \
@@ -337,11 +337,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 
@@ -403,13 +403,14 @@ 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: library/libnames.cmi kernel/names.cmi \
-    contrib/first-order/sequent.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/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/sequent.cmi \
-    kernel/term.cmi 
+contrib/first-order/unify.cmi: contrib/first-order/formula.cmi \
+    library/libnames.cmi contrib/first-order/sequent.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 \
@@ -481,6 +482,14 @@ 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/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/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 \
@@ -503,14 +512,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.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/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 
@@ -655,6 +656,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 \
@@ -663,12 +670,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 \
@@ -751,10 +752,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 
@@ -763,24 +764,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 \
@@ -885,6 +876,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 
@@ -2001,10 +2002,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 \
@@ -2209,18 +2210,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 \
@@ -2281,6 +2270,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 \
@@ -2355,6 +2356,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 \
@@ -2371,18 +2384,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 \
@@ -2758,7 +2759,7 @@ contrib/first-order/engine.cmo: tactics/auto.cmi toplevel/cerrors.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 
+    kernel/term.cmi contrib/first-order/unify.cmi lib/util.cmi 
 contrib/first-order/engine.cmx: tactics/auto.cmx toplevel/cerrors.cmx \
     parsing/egrammar.cmx parsing/extend.cmx contrib/first-order/formula.cmx \
     interp/genarg.cmx library/libnames.cmx parsing/pcoq.cmx lib/pp.cmx \
@@ -2766,7 +2767,7 @@ contrib/first-order/engine.cmx: tactics/auto.cmx toplevel/cerrors.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 
+    kernel/term.cmx contrib/first-order/unify.cmx lib/util.cmx 
 contrib/first-order/formula.cmo: interp/coqlib.cmi kernel/declarations.cmi \
     library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
     library/libnames.cmi kernel/names.cmi pretyping/reductionops.cmi \
@@ -2804,13 +2805,15 @@ contrib/first-order/sequent.cmx: tactics/auto.cmx interp/constrextern.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 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/formula.cmi library/libnames.cmi kernel/names.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 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 
+    contrib/first-order/formula.cmx library/libnames.cmx kernel/names.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 
 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 \
@@ -3031,6 +3034,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 \
@@ -3055,14 +3066,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 \
@@ -3293,12 +3296,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 \
@@ -3353,8 +3356,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 \
@@ -3379,10 +3380,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 
@@ -3393,6 +3392,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/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4
index 07864fe9bf..612ac309b7 100644
--- a/contrib/first-order/engine.ml4
+++ b/contrib/first-order/engine.ml4
@@ -56,12 +56,16 @@ let ground_tac solver startseq gl=
 	    (or_tac toptac (re_add seq))
 	    (left_tac seq ctx) gl
 	| Rexists(i,dom)->
-	    tclORELSE
-	    (if seq.depth<=0 || not !qflag then 
-	       tclFAIL 0 "max depth" 
-	     else 
-	       exists_tac i dom atoms toptac (re_add seq))
-	    (left_tac seq ctx) gl
+	    let cont_tac=left_tac seq ctx in
+	      if seq.depth<=0 || not !qflag then 
+		cont_tac gl
+	      else 
+		(match Unify.give_right_instances i dom atoms seq with
+		    Some l -> tclORELSE
+		      (exists_tac l toptac (re_add seq)) cont_tac gl
+		  | None ->
+		      tclORELSE cont_tac
+		      (dummy_exists_tac dom  toptac (re_add seq)) gl)
 	| _-> anomaly "unreachable place"
   and left_tac seq ctx gl=
     if is_empty_left seq then 
@@ -77,13 +81,13 @@ let ground_tac solver startseq gl=
 	  | Lor ind->
 	      left_or_tac ind hd.id toptac (re_add seq1) gl
 	  | Lforall (i,dom)->
-	      tclORELSE
-	      (if seq.depth<=0 || not !qflag then 
-		 tclFAIL 0 "max depth" 
-	       else 
-		 left_forall_tac i dom hd.atoms hd.internal hd.id
-		    toptac (re_add seq))
-	      (left_tac seq1 (hd::ctx)) gl
+	      let (lfp,seq2)=collect_forall seq in
+		tclORELSE
+		  (if seq.depth<=0 || not !qflag then 
+		     tclFAIL 0 "max depth" 
+		   else 
+		     left_forall_tac lfp toptac (re_add seq))
+		  (left_tac seq2 (lfp@ctx)) gl
 	  | Lexists ->
 	      if !qflag then
 		left_exists_tac hd.id toptac (re_add seq1) gl
@@ -130,18 +134,23 @@ let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
 let fail_solver=tclFAIL 0 "GroundTauto failed"
 		      
 let gen_ground_tac flag taco io l=
-  qflag:=flag;
-  let depth=
-    match io with 
-	Some i->i
-      | None-> !Auto.default_search_depth in
-  let solver= 
-    match taco with 
-	Some tac->tac
-      | None-> default_solver in
-  let startseq=create_with_ref_list l depth in
-    ground_tac solver startseq
-
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let depth=
+	match io with 
+	    Some i->i
+	  | None-> !Auto.default_search_depth in
+      let solver= 
+	match taco with 
+	    Some tac->tac
+	  | None-> default_solver in
+      let startseq=create_with_ref_list l depth in
+      let result=
+	ground_tac solver startseq
+      in qflag:=backup;result
+    with e -> qflag:=backup;raise e
+	   
 open Genarg
 open Pcoq
 open Pp
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 196f11bf55..aaf195a43a 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -20,7 +20,13 @@ open Libnames
 
 let qflag=ref true
 
-let (+-) i j=if i=0 then j else i
+let (=?) f g i1 i2 j1 j2=
+  let c=f i1 i2 in
+    if c=0 then g j1 j2 else c
+
+let (==?) fg h i1 i2 j1 j2 k1 k2=
+  let c=fg i1 i2 j1 j2 in
+    if c=0 then h k1 k2 else c
 
 type ('a,'b)sum=Left of 'a|Right of 'b
 	
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 1f9d653b2f..1e23d7c0bc 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -14,7 +14,11 @@ open Libnames
 
 val qflag : bool ref
 
-val (+-) : int -> int -> int
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
+  'a -> 'a -> 'b -> 'b -> int
+  
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
+  'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 00a6fe89df..ebd820bcc9 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -95,25 +95,35 @@ let left_or_tac ind id tacrec seq=
       (Array.map f v)
 
 let forall_tac tacrec seq=
-  tclTHEN intro (wrap 0 true tacrec seq)
+  tclTHEN intro (wrap 1 true tacrec seq)
 
-let left_forall_tac i dom atoms internal id tacrec seq=
-  let insts=find_instances i atoms seq in
-    if insts=[] then
-      if internal && not (lookup id None seq) then
-	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]
-      else tclFAIL 0 "no phantom variable for external hyp"
-    else
-      let tac t=
+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(i,dom)-> 
+	     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
@@ -122,29 +132,34 @@ let left_forall_tac i dom atoms internal id tacrec seq=
 	     intro; 
 	     tclSOLVE 
 	       [wrap 1 false tacrec 
-		  (deepen (record id (Some t) seq))]] in
-	tclFIRST (List.map tac insts)
+		  (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 arrow_tac tacrec seq=
   tclTHEN intro (wrap 1 true tacrec seq)
-    
-let exists_tac i dom atoms tacrec seq=
-  let insts=find_instances i atoms seq in
-    if insts=[] then 
-      tclTHENS (cut dom) 
+   
+
+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]
-	 else
-	   let tac t=
-	     tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	       (tclSOLVE [wrap 0 true tacrec (deepen seq)]) in
-	     tclFIRST (List.map tac insts)
-	       
+	    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
+
 let left_exists_tac id tacrec seq=
   tclTHENLIST
     [simplest_elim (constr_of_reference id);
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 7dbd5f556b..692443baed 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -37,11 +37,19 @@ val left_or_tac : inductive -> lseqtac
 
 val forall_tac : seqtac
 
-val left_forall_tac : int -> types -> (bool * constr) list -> bool -> lseqtac
+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 exists_tac : int -> types -> (bool * constr) list -> seqtac
+val dummy_exists_tac : constr -> seqtac
+
+val right_instance_tac : constr * int -> seqtac
+
+val exists_tac : (constr * int) list -> seqtac
 	       
 val left_exists_tac : lseqtac
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 678c35a950..1684716d1f 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -52,27 +52,83 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
+(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let rec compare_list f l1 l2=
+  match l1,l2 with
+      [],[]-> 0
+    | [],_ -> -1
+    | _,[] -> 1
+    | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
+
+
+let compare_array f v1 v2=  
+  let l=Array.length v1 in
+  let c=l - Array.length v2 in
+    if c=0 then
+      let rec comp_aux i=
+	if i<0 then 0 
+	else
+	  let ci=f v1.(i) v2.(i) in
+	    if ci=0 then 
+	      comp_aux (i-1)
+	    else ci
+      in comp_aux (l-1)
+    else c
+
+let compare_constr_int f t1 t2 =
+  match kind_of_term t1, kind_of_term t2 with
+    | Rel n1, Rel n2 -> n1 - n2
+    | Meta m1, Meta m2 -> m1 - m2
+    | Var id1, Var id2 -> Pervasives.compare id1 id2
+    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
+    | Cast (c1,_), _ -> f c1 t2
+    | _, Cast (c2,_) -> f t1 c2
+    | Prod (_,t1,c1), Prod (_,t2,c2) 
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	(f =? f) t1 t2 c1 c2 
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
+	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
+    | App (_,_), App (_,_) ->
+	let c1,l1=decompose_app t1 
+	and c2,l2=decompose_app t2 in
+	  (f =? (compare_list f)) c1 c2 l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> 
+	((-) =? (compare_array f)) e1 e2 l1 l2
+    | Const c1, Const c2 -> Pervasives.compare c1 c2
+    | Ind c1, Ind c2 -> Pervasives.compare c1 c2
+    | Construct c1, Construct c2 -> Pervasives.compare c1 c2
+    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+	((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2
+    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
+	ln1 ln2 tl1 tl2 bl1 bl2
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
+	ln1 ln2 tl1 tl2 bl1 bl2
+    | _ -> Pervasives.compare t1 t2
+
+let rec compare_constr m n=
+  compare_constr_int compare_constr m n
+    
 module OrderedConstr=
 struct
   type t=constr
-  let rec compare c1 c2=
-    match (kind_of_term c1,kind_of_term c2) with
-	(Prod(_,a1,b1),Prod(_,a2,b2))
-      | (Lambda(_,a1,b1),Lambda(_,a2,b2)) ->
-	  (compare a1 a2) +- (compare b1 b2)
-      | (LetIn(_,a1,b1,aa1),LetIn(_,a2,b2,aa2)) ->
- 	  ((compare a1 a2) +- (compare b1 b2)) +- (compare aa1 aa2)
-      | _-> Pervasives.compare c1 c2
+  let compare=compare_constr
 end
 
 module Hitem=
 struct 
   type t=(global_reference * constr option)
   let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare id1 id2) +- 
-    (match co1,co2 with
-	 Some c1,Some c2 -> OrderedConstr.compare c1 c2
-       | _->Pervasives.compare co1 co2)
+    (Pervasives.compare 
+     =? (fun oc1 oc2 ->
+	   match oc1,oc2 with 
+	       Some c1,Some c2 -> OrderedConstr.compare c1 c2
+	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
 end
 
 module CM=Map.Make(OrderedConstr)
@@ -185,7 +241,6 @@ let create_with_auto_hints depth gl=
     !seqref
 
 let print_cmap map=
-  
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
       str "| " ++ 
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 751c297453..851396d45a 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -19,6 +19,8 @@ val right_reversible : right_pattern -> bool
 	
 val left_reversible : left_pattern -> bool
 
+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
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 0c336b6d31..5c0148d1f1 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -13,6 +13,7 @@ open Formula
 open Sequent
 open Tacmach
 open Term
+open Names
 open Termops
 open Reductionops
 
@@ -80,71 +81,161 @@ let unif t1 t2= (* Martelli-Montanari style *)
       assert false 
 	(* 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 collect i l=
-  try
-    let t=List.assoc i l in 
-      if is_ground t then Some t else None
-  with Not_found->None
+let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
 
-let value i=
+let value i t=
+  let add x y=
+    if x<0 then y else if y<0 then x else x+y in
   let tref=mkMeta i in
   let rec vaux term=
-    if term=tref then 1 else 
-      let f v t=max v (vaux t) in
-      let vrec=fold_constr f 0 term in
-	if vrec=0 then 0 else succ vrec in vaux
+    if term=tref then 0 else 
+      let f v t=add v (vaux t) in
+      let vr=fold_constr f (-1) term in
+	if vr<0 then -1 else vr+1 in
+    vaux t
+	  
+type instance=
+    Real of constr*int (* instance*valeur heuristique*)
+  | Phantom of constr (* domaine de quantification *)
+ 	  
+let unif_atoms i dom t1 t2=
+  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
+    with
+	UFAIL(_,_) ->None
+      | Not_found ->Some (Phantom dom)
+      
+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
 
-let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
+module OrderedRightInstance=
+struct 
+  type t = constr*int
+  let compare (c1,n1) (c2,n2) = ((-) =? OrderedConstr.compare) n2 n1 c1 c2
+end
 
-let unif_atoms_for_meta i (b1,t1) (b2,t2)=
-  if b1=b2  || is_head_meta t1 || is_head_meta t2  then None else
-    try 
-       match collect i (unif t1 t2) with
-	   None->None
-	 | Some t->Some ((max (value i t1) (value i t2)),t)
-    with UFAIL(_,_) ->None
-    
-module OrderedConstr=
+module OrderedLeftInstance=
 struct
-  type t=int*constr
-  let compare (n1,t1) (n2,t2)=
-    (n2 - n1) +- (Pervasives.compare t1 t2) 
-    (* we want a decreasing total order *)
+  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 CS=Set.Make(OrderedConstr)
+module RIS=Set.Make(OrderedRightInstance)
+module LIS=Set.Make(OrderedLeftInstance)
   
-let match_atom_list i atom l=
-  let f atom2 accu=
-    match unif_atoms_for_meta i atom atom2 with
-	None-> accu
-      | Some t-> CS.add t accu in
-    List.fold_right f l CS.empty
-
-let match_lists i l1 l2=
-  let f atom accu=
-    CS.union (match_atom_list i atom l2) accu in
-    List.fold_right f l1 CS.empty
-      
-let find_instances i l seq=
-  let match_hyp f accu=
-    CS.union 
-      (if f.internal then 
-	 match_lists i l f.atoms 
-       else 
-	 CS.empty) 
-      accu in
-  let match_atom t accu=
-    CS.union (match_atom_list i (false,t) l) accu in
-  let s1=
-    match seq.gl with 
-	Atomic t->(match_atom_list i (true,t) l)
-      | Complex(_,_,l1)->(match_lists i l l1) in
-  let s2=List.fold_right match_atom seq.latoms s1 in
-  let s3=HP.fold match_hyp seq.redexes s2 in
-    List.map snd (CS.elements s3)
+(* le premier argument est une sous formule a instancier *)
+
+let match_atom_with_latoms i dom (pol,atom) latoms accu=
+  if pol then 
+    let f latom accu=
+      match unif_atoms i dom atom latom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
+      List.fold_right f latoms accu
+  else accu 
+
+let match_atom_with_hyp_atoms i dom (pol,atom) lf accu=
+  let f (b,hatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom hatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i))->(false,RIS.add (t,i) (snd accu)) in
+    List.fold_right f lf.atoms accu
+
+let match_atom_with_goal i dom (pol,atom) glatoms accu=
+  let f (b,glatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom glatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some (Real(t,i)) ->(false,RIS.add (t,i) (snd accu)) in
+    List.fold_right f glatoms accu
+
+let give_right_instances i dom ratoms seq=
+  let f ratom accu=
+    let accu1= match_atom_with_goal i dom ratom ratoms accu in
+    let accu2=
+      match_atom_with_latoms i dom ratom seq.latoms accu1 in
+      HP.fold (match_atom_with_hyp_atoms i dom ratom) seq.redexes accu2 in
+  let (b,accu0)=List.fold_right f ratoms (false,RIS.empty) in
+    if b & RIS.is_empty accu0 then 
+      None
+    else
+      Some (RIS.elements accu0)
+
+(*left*) 
+	  
+let match_named_atom_with_latoms id i dom (pol,atom) latoms accu=
+  if pol then 
+    let f latom accu=
+      match unif_atoms i dom atom latom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some inst ->(false,LIS.add (inst,id) (snd accu)) in
+      List.fold_right f latoms accu
+  else accu 
+
+let match_named_atom_with_hyp_atoms id i dom (pol,atom) lf accu=
+  let f (b,hatom) accu=
+    if b=pol then accu else
+      match unif_atoms i dom atom hatom with
+	  None->accu
+	| Some (Phantom _) ->(true,snd accu)
+	| Some inst->(false,LIS.add (inst,id) (snd accu)) in
+    List.fold_right f lf.atoms accu
+
+let match_named_atom_with_goal id i dom (pol,atom) gl accu=
+  match gl with 
+      Atomic t->
+	if pol then accu else
+	  (match unif_atoms i dom atom t with
+	       None->accu
+	     | Some (Phantom _) ->(true,snd accu)
+	     | Some inst ->(false,LIS.add (inst,id) (snd accu)))
+    | Complex (_,_,glatoms)->
+	let f (b,glatom) accu=
+	  if b=pol then accu else
+	    match unif_atoms i dom atom glatom with
+		None->accu
+	      | Some (Phantom _) ->(true,snd accu)
+	      | Some inst ->(false,LIS.add (inst,id) (snd accu)) in
+	  List.fold_right f glatoms accu
+
+let match_one_forall_hyp seq lf accu=
+  match lf.pat with 
+      Lforall(i,dom)->
+	let f latom accu=
+	  let accu1=match_named_atom_with_goal lf.id i dom latom seq.gl accu in
+	  let accu2=
+	    match_named_atom_with_latoms lf.id i dom latom seq.latoms accu1 in
+	    HP.fold (match_named_atom_with_hyp_atoms lf.id i dom latom) 
+	      seq.redexes accu2 in
+	let (b,accu0)=List.fold_right f lf.atoms (false,LIS.empty) in
+	  if b & LIS.is_empty accu0 then 
+	    LIS.add (Phantom dom,lf.id) accu
+	  else
+	    LIS.union accu0 accu
+    | _ ->anomaly "can't happen" 
+
+let give_left_instances lfh seq=
+  LIS.elements (List.fold_right (match_one_forall_hyp seq) lfh LIS.empty)
 
+(* TODO: match with goal *)
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 5423884886..281e940630 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -8,9 +8,17 @@
 
 (* $Id$ *)
 
+open Libnames
 open Term
 
-val unif_atoms_for_meta : int -> (bool * constr) -> (bool * constr) ->
-  (int*constr) option
+type instance=
+    Real of constr*int (* instance*valeur heuristique*)
+  | Phantom of constr (* domaine de quantification *)
 
-val find_instances : int -> (bool * constr) list -> Sequent.t -> constr list
+val unif_atoms : int -> constr -> constr -> constr -> instance option
+  
+val give_right_instances : int -> constr -> (bool * constr) list -> 
+  Sequent.t -> (constr*int) list option
+
+val give_left_instances : Formula.left_formula list-> Sequent.t -> 
+  (instance*global_reference) list