Enhancement of the Ground tactic, addition of GTauto and GIntuition.

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

11 files changed, 668 insertions, 381 deletions

diff --git a/.depend b/.depend
index ed7da896f6..9bfa91cb95 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 
@@ -402,10 +402,9 @@ contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
 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 \
-    kernel/sign.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 
+    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/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 
@@ -480,6 +479,12 @@ 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.cmo ide/coq.cmi ide/coq_commands.cmo \
+    ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmo proofs/pfedit.cmi \
+    ide/preferences.cmo ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo 
+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/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi ide/ideutils.cmo library/lib.cmi kernel/names.cmi \
@@ -496,12 +501,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     proofs/refiner.cmx library/states.cmx proofs/tacmach.cmx kernel/term.cmx \
     lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
     toplevel/vernacexpr.cmx ide/coq.cmi 
-ide/coqide.cmo: ide/command_windows.cmo ide/coq.cmi ide/coq_commands.cmo \
-    ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmo proofs/pfedit.cmi \
-    ide/preferences.cmo ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo 
-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/find_phrase.cmo: ide/ideutils.cmo 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmo 
@@ -646,6 +645,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 \
@@ -654,12 +659,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 \
@@ -742,10 +741,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 
@@ -754,24 +753,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 \
@@ -876,6 +865,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 
@@ -1992,10 +1991,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 \
@@ -2200,18 +2199,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 \
@@ -2272,6 +2259,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 \
@@ -2344,6 +2343,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 \
@@ -2360,18 +2371,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 \
@@ -2741,48 +2740,54 @@ contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \
     interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
 contrib/first-order/engine.cmo: tactics/auto.cmi toplevel/cerrors.cmi \
-    parsing/egrammar.cmi contrib/first-order/formula.cmi interp/genarg.cmi \
-    parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/refiner.cmi \
-    contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
-    proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+    parsing/egrammar.cmi parsing/extend.cmi contrib/first-order/formula.cmi \
+    interp/genarg.cmi library/libnames.cmi parsing/pcoq.cmi lib/pp.cmi \
+    parsing/pptactic.cmi proofs/refiner.cmi contrib/first-order/rules.cmi \
+    contrib/first-order/sequent.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
 contrib/first-order/engine.cmx: tactics/auto.cmx toplevel/cerrors.cmx \
-    parsing/egrammar.cmx contrib/first-order/formula.cmx interp/genarg.cmx \
-    parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/refiner.cmx \
-    contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
-    proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+    parsing/egrammar.cmx parsing/extend.cmx contrib/first-order/formula.cmx \
+    interp/genarg.cmx library/libnames.cmx parsing/pcoq.cmx lib/pp.cmx \
+    parsing/pptactic.cmx proofs/refiner.cmx contrib/first-order/rules.cmx \
+    contrib/first-order/sequent.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.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 \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
-    lib/util.cmi contrib/first-order/formula.cmi 
+    proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    contrib/first-order/formula.cmi 
 contrib/first-order/formula.cmx: interp/coqlib.cmx kernel/declarations.cmx \
     library/global.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
     library/libnames.cmx kernel/names.cmx pretyping/reductionops.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
-    lib/util.cmx contrib/first-order/formula.cmi 
+    proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    contrib/first-order/formula.cmi 
 contrib/first-order/rules.cmo: kernel/declarations.cmi \
     contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
     pretyping/rawterm.cmi pretyping/reductionops.cmi \
-    contrib/first-order/sequent.cmi kernel/sign.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/sequent.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    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: kernel/declarations.cmx \
     contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
     pretyping/rawterm.cmx pretyping/reductionops.cmx \
-    contrib/first-order/sequent.cmx kernel/sign.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 
-contrib/first-order/sequent.cmo: tactics/auto.cmi \
-    contrib/first-order/formula.cmi lib/heap.cmi library/libnames.cmi \
-    kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
+    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 contrib/first-order/unify.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 
-contrib/first-order/sequent.cmx: tactics/auto.cmx \
-    contrib/first-order/formula.cmx lib/heap.cmx library/libnames.cmx \
-    kernel/names.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
+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 pretyping/reductionops.cmi \
@@ -3012,6 +3017,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 \
@@ -3036,14 +3049,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 \
@@ -3274,12 +3279,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 \
@@ -3334,8 +3339,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 \
@@ -3360,10 +3363,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 
@@ -3374,6 +3375,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 133fbe1229..26abbc63bb 100644
--- a/contrib/first-order/engine.ml4
+++ b/contrib/first-order/engine.ml4
@@ -17,100 +17,172 @@ open Term
 open Tacmach
 open Tactics
 open Tacticals
+open Libnames
 open Util
 
-let ground_tac ninst solver gl=
-  let metagen=newcnt () in
-  let rec toptac ninst seq gl=
+(* 
+   1- keep track of the instantiations and of ninst in the Sequent.t structure 
+   2- ordered instantiations
+*)
+
+let ground_tac solver startseq gl=
+  let rec toptac seq gl=
     match seq.gl with 
 	Atomic t->
-	  tclORELSE (axiom_tac t seq) (left_tac ninst seq []) gl
-      | Complex (pat,l)->
-	  match pat with
-	      Rand->and_tac seq (toptac ninst) metagen gl
-	    | Rforall->forall_tac seq (toptac ninst) metagen gl
-	    | Rarrow->arrow_tac seq (toptac ninst) metagen gl
-	    | _->
-		if not (is_empty_left seq) && rev_left seq then 
-		  left_tac ninst seq [] gl 
-		else 
-		  right_tac ninst seq pat l [] gl
-  and right_tac ninst seq pat atoms ctx gl=
+	  tclORELSE (axiom_tac t seq) (left_tac seq []) gl
+      | Complex (pat,t,l)->
+	  tclORELSE (axiom_tac t seq)
+	  (match pat with
+	       Rand->
+		 and_tac toptac seq
+	     | Rforall->
+		 forall_tac toptac seq
+	     | Rarrow->
+		 arrow_tac toptac seq
+	     | Revaluable egr->
+		 evaluable_tac egr toptac seq
+	     | _->
+		 if not (is_empty_left seq) && rev_left seq then 
+		   left_tac seq [] 
+		 else 
+		   right_tac seq pat l []) gl
+  and right_tac seq pat atoms ctx gl=
     let re_add s=re_add_left_list ctx s in
       match pat with
 	  Ror->
 	    tclORELSE
-	    (or_tac (re_add seq) (toptac ninst) metagen)
-	    (left_tac ninst seq ctx) gl
+	    (or_tac toptac (re_add seq))
+	    (left_tac seq ctx) gl
 	| Rexists(i,dom)->
 	    tclORELSE
-	    (if ninst=0 then tclFAIL 0 "max depth" else 
-	       exists_tac i dom atoms (re_add seq) (toptac (ninst-1)) metagen)
-	    (left_tac ninst seq ctx) gl
+	    (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
 	| _-> anomaly "unreachable place"
-  and left_tac ninst seq ctx gl=
+  and left_tac seq ctx gl=
     if is_empty_left seq then 
       solver gl (* put solver here *)
     else 
       let (hd,seq1)=take_left seq in 
       let re_add s=re_add_left_list ctx s in 
 	match hd.pat with
-	    Lfalse->left_false_tac hd.id gl
-	  | Land ind->left_and_tac ind hd.id seq1 (toptac ninst) metagen gl
-	  | Lor ind->left_or_tac ind hd.id seq1 (toptac ninst) metagen gl
+	    Lfalse->
+	      left_false_tac hd.id gl
+	  | Land ind->
+	      left_and_tac ind hd.id toptac (re_add seq1) gl
+	  | Lor ind->
+	      left_or_tac ind hd.id toptac (re_add seq1) gl
 	  | Lforall (i,dom)->
 	      tclORELSE
-	      (if ninst=0 then tclFAIL 0 "max depth" else 
-		 left_forall_tac i dom hd.atoms hd.id (re_add seq)
-		   (toptac (ninst-1)) metagen)
-	      (left_tac ninst seq1 (hd::ctx)) gl
-	  | Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl
-	  | LAatom a->
-	      tclORELSE
-	      (ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen)
-	      (match seq1.gl with 
-		  Atomic t->
-		    (left_tac ninst seq1 (hd::ctx))
-		| Complex (pat,atoms)->
-		    (right_tac ninst seq1 pat atoms (hd::ctx))) gl
-	  | LAfalse->ll_false_tac hd.id seq1 (toptac ninst) metagen gl
-	  | LAand (ind,largs) | LAor(ind,largs) ->
-	      ll_ind_tac ind largs hd.id seq1 (toptac ninst) metagen gl
-	  | LAforall p ->	      
+	      (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
+	  | Lexists ->
+	      if !qflag then
+		left_exists_tac hd.id toptac (re_add seq1) gl
+	      else (left_tac seq1 (hd::ctx)) gl
+	  | Levaluable egr->
+	      left_evaluable_tac egr hd.id toptac (re_add seq1) gl
+	  | LA (typ,lap)->
 	      tclORELSE
-	      (if ninst=0 then tclFAIL 0 "max depth" else 
-		 ll_forall_tac p hd.id (re_add seq1) 
-		   (toptac (ninst-1)) metagen)
-	      (left_tac ninst seq1 (hd::ctx)) gl
-	  | LAexists (ind,a,p,_) ->
-	      ll_ind_tac ind [a;p] hd.id seq1 (toptac ninst) metagen gl
-	  | LAarrow (a,b,c) ->	      
-	      tclORELSE
-	      (ll_arrow_tac a b c hd.id (re_add seq1) 
-		   (toptac ninst) metagen)
-	      (left_tac ninst seq1 (hd::ctx)) gl in
-  let startseq=create_with_auto_hints gl metagen in
-    wrap (List.length (pf_hyps gl)) true empty_seq (toptac ninst) metagen gl
-
+	      (ll_atom_tac typ hd.id toptac (re_add seq1))
+	      (match lap with
+		   LLatom->
+		     (match seq1.gl with 
+			  Atomic t->
+			    (left_tac seq1 (hd::ctx))
+			| Complex (pat,_,atoms)->
+			    (right_tac seq1 pat atoms (hd::ctx))) 
+		 | LLfalse->
+		     ll_false_tac hd.id toptac (re_add seq1) 
+		 | LLand (ind,largs) | LLor(ind,largs) ->
+		     ll_ind_tac ind largs hd.id toptac (re_add seq1) 
+		 | LLforall p ->	      
+		     tclORELSE
+		     (if seq.depth<=0 || not !qflag then 
+			tclFAIL 0 "max depth" 
+		      else 
+			ll_forall_tac p hd.id toptac (re_add seq1))
+		     (left_tac seq1 (hd::ctx))
+		 | LLexists (ind,a,p,_) ->
+		     if !qflag then
+		       ll_ind_tac ind [a;p] hd.id toptac (re_add seq1) 
+		     else
+		       left_tac seq1 (hd::ctx)
+		 | LLarrow (a,b,c) ->	      
+		     tclORELSE
+		     (ll_arrow_tac a b c hd.id toptac (re_add seq1))
+		     (left_tac seq1 (hd::ctx))
+		 | LLevaluable egr->
+		     left_evaluable_tac egr hd.id toptac (re_add seq1))
+	      gl in
+    wrap (List.length (pf_hyps gl)) true toptac (startseq gl) gl
+      
 let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
-		     
-let gen_ground_tac io taco=
-   let depth=
-     match io with 
-	 Some i->i
-       | None-> !Auto.default_search_depth in
-   let solver= 
-     match taco with 
-	 Some t->snd t
-       | None-> default_solver in
-     ground_tac depth default_solver
+    
+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
+
+open Genarg
+open Pcoq
+open Pp
+
+type depth=int option
+
+let pr_depth _ _=function
+    None->mt ()
+  | Some i -> str " depth " ++ int i
+
+ARGUMENT EXTEND depth TYPED AS depth PRINTED BY pr_depth
+[ "depth" integer(i)]-> [ Some i]
+| [ ] -> [None]
+END 
+
+type with_reflist = global_reference list
+
+let pr_ref_list _ _=function
+    [] -> mt ()
+  | l -> prlist pr_reference l
 
 TACTIC EXTEND Ground
-   [ "Ground" ] -> [ gen_ground_tac None None ]    
-|  [ "Ground" integer(n)] -> [ gen_ground_tac (Some n) None]
-|  [ "Ground" tactic(t)] -> [ gen_ground_tac None (Some t)]    
-|  [ "Ground" integer(n) tactic(t)] -> 
-     [ gen_ground_tac (Some n) (Some t) ]
+   [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) None l ]
+|   [ "Ground" tactic(t) "depth" integer(i) "with" ne_reference_list(l) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) (Some i) l ]
+|   [ "Ground" tactic(t) "depth" integer(i) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) (Some i) [] ]
+|   [ "Ground" tactic(t) ] -> 
+	 [ gen_ground_tac true (Some (snd t)) None [] ]
+|   [ "Ground" ] ->
+	 [ gen_ground_tac true None None [] ]
+END
+
+TACTIC EXTEND GTauto   
+  [ "GTauto" ] ->
+     [ gen_ground_tac false (Some fail_solver) (Some 0) [] ]   
+END
+
+TACTIC EXTEND GIntuition
+   ["GIntuition" tactic(t)] ->
+     [ gen_ground_tac false (Some(snd t)) None [] ]
+|  [ "GIntuition" ] ->
+     [ gen_ground_tac false None None [] ] 
 END
 
- 
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index e6406f107b..196f11bf55 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -18,8 +18,12 @@ open Util
 open Declarations
 open Libnames
 
-type ('a,'b)sum=Left of 'a|Right of 'b
+let qflag=ref true
+
+let (+-) i j=if i=0 then j else i
 
+type ('a,'b)sum=Left of 'a|Right of 'b
+	
 type kind_of_formula=
    Arrow of constr*constr
   |And of inductive*constr list
@@ -27,14 +31,11 @@ type kind_of_formula=
   |Exists of inductive*constr*constr*constr
   |Forall of constr*constr
   |Atom of constr
+  |Evaluable of evaluable_global_reference*constr
   |False
 
 type counter = bool -> int
 
-let newcnt ()=
-  let cnt=ref (-1) in
-    fun b->if b then incr cnt;!cnt
-
 let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str
 
 let op2bool=function Some _->true |None->false
@@ -44,7 +45,8 @@ let id_sig=constant "Specif" "sig"
 let id_sigT=constant "Specif" "sigT"
 let id_sigS=constant "Specif" "sigS"
 let id_not=constant "Logic" "not"
- 
+let id_iff=constant "Logic" "iff"
+
 let is_ex t = 
   t=(id_ex ()) || 
     t=(id_sig ()) || 
@@ -62,13 +64,14 @@ let match_with_exist_term t=
 	else None
     | _->None
 
-let match_with_not_term t=
-  match match_with_nottype t with 
-    | None ->
-	(match kind_of_term t with
-	     App (no,b) when no=id_not ()->Some (no,b.(0))
-	   | _->None)
-    | o -> o
+let match_with_evaluable t=
+  match kind_of_term t with
+      App (hd,b)-> 
+	if (hd=id_not () && (Array.length b) = 1) ||
+	  (hd=id_iff () && (Array.length b) = 2) then 
+	    Some(destConst hd,t)
+	else None
+    | _-> None
 
 let rec nb_prod_after n c=
   match kind_of_term c with
@@ -78,8 +81,8 @@ let rec nb_prod_after n c=
 
 let nhyps mip = 
   let constr_types = mip.mind_nf_lc in 
-  let nhyps = nb_prod_after mip.mind_nparams in	
-    Array.map nhyps constr_types
+  let hyp = nb_prod_after mip.mind_nparams in	
+    Array.map hyp constr_types
 
 let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))
     
@@ -111,19 +114,23 @@ let kind_of_formula cciterm =
 		Some (i,a,b,p)-> Exists((destInd i),a,b,p)
 	      |_-> 
 		 match match_with_nodep_ind cciterm with
-		     None -> Atom cciterm 
-		   | Some (i,l)->
+		     Some (i,l)->
 		       let ind=destInd i in
 		       let (mib,mip) = Global.lookup_inductive ind in
 			 if Inductiveops.mis_is_recursive (ind,mib,mip) then
 			   Atom cciterm 
 			 else
-			   match Array.length mip.mind_consnames with
-			       0->False
-			     | 1->And(ind,l)
-			     | _->Or(ind,l) 
+			   (match Array.length mip.mind_consnames with
+				0->False
+			      | 1->And(ind,l)
+			      | _->Or(ind,l)) 
+		   | None -> 
+		       match match_with_evaluable cciterm with 
+			   Some (cst,t)->Evaluable ((EvalConstRef cst),t)
+			 | None ->Atom cciterm
 
-let build_atoms metagen=
+ 
+let build_atoms gl metagen=
   let rec build_rec env polarity cciterm =
     match kind_of_formula cciterm with
 	False->[]
@@ -132,19 +139,22 @@ let build_atoms metagen=
 	  (build_rec env polarity b)
       | And(i,l) | Or(i,l)->
 	  (try
-	    let v = ind_hyps i l in
-	      Array.fold_right
-		(fun l accu->
-		   List.fold_right 
-		   (fun (_,_,t) accu0->
-		      (build_rec env polarity t)@accu0) l accu) v []
-	  with Dependent_Inductive ->
-	    [polarity,(substnl env 0 cciterm)])
+	     let v = ind_hyps i l in
+	     let g i accu (_,_,t) =
+	       (build_rec env polarity (lift i t))@accu in
+	     let f l accu =
+	       list_fold_left_i g (1-(List.length l)) accu l in
+	       Array.fold_right f v [] 
+	   with Dependent_Inductive ->
+	     [polarity,(substnl env 0 cciterm)])
       | Forall(_,b)|Exists(_,_,b,_)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b 
       | Atom t->
 	  [polarity,(substnl env 0 cciterm)]
+      | Evaluable(ec,t)->
+	  let nt=Tacred.unfoldn [[1],ec] (pf_env gl) (Refiner.sig_sig gl) t in
+	  build_rec env polarity nt
   in build_rec []
        
 type right_pattern =
@@ -153,33 +163,40 @@ type right_pattern =
   | Rforall
   | Rexists of int*constr
   | Rarrow
+  | Revaluable of evaluable_global_reference
       
 type right_formula =
-    Complex of right_pattern*((bool*constr) list)
+    Complex of right_pattern*constr*((bool*constr) list)
   | Atomic of constr
       
+type left_arrow_pattern=
+    LLatom
+  | LLfalse
+  | LLand of inductive*constr list
+  | LLor of inductive*constr list
+  | LLforall of constr
+  | LLexists of inductive*constr*constr*constr
+  | LLarrow of constr*constr*constr
+  | LLevaluable of evaluable_global_reference
+
 type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
   | Lforall of int*constr
   | Lexists
-  | LAatom of constr
-  | LAfalse
-  | LAand of inductive*constr list
-  | LAor of inductive*constr list
-  | LAforall of constr
-  | LAexists of inductive*constr*constr*constr
-  | LAarrow of constr*constr*constr
-      
+  | Levaluable of evaluable_global_reference
+  | LA of constr*left_arrow_pattern
+
 type left_formula={id:global_reference;
+		   constr:constr;
 		   pat:left_pattern;
 		   atoms:(bool*constr) list;
 		   internal:bool}
     
 exception Is_atom of constr
 
-let build_left_entry nam typ internal metagen=
+let build_left_entry nam typ internal gl metagen=
   try 
     let pattern=
       match kind_of_formula typ with
@@ -189,20 +206,29 @@ let build_left_entry nam typ internal metagen=
 	| Or(i,_)          ->  Lor i
 	| Exists (_,_,_,_) ->  Lexists
 	| Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d)
-	| Arrow (a,b) ->
-	    (match kind_of_formula a with
-		 False->      LAfalse
-	       | Atom a->     LAatom a
-	       | And(i,l)->      LAand(i,l)
-	       | Or(i,l)->       LAor(i,l)
-	       | Arrow(a,c)-> LAarrow(a,c,b)
-	       | Exists(i,a,_,p)->LAexists(i,a,p,b)
-	       | Forall(_,_)->LAforall a) in    
-    let l=build_atoms metagen false typ in
-      Left {id=nam;pat=pattern;atoms=l;internal=internal}
+	| Evaluable (egc,_) ->Levaluable egc 
+	| Arrow (a,b) ->LA (a, 
+			    match kind_of_formula a with
+				False->      LLfalse
+			      | Atom t->     LLatom
+			      | And(i,l)->      LLand(i,l)
+			      | Or(i,l)->       LLor(i,l)
+			      | Arrow(a,c)-> LLarrow(a,c,b)
+			      | Exists(i,a,_,p)->LLexists(i,a,p,b)
+			      | Forall(_,_)->LLforall a
+			      | Evaluable (egc,_)-> LLevaluable egc) in    
+    let l=
+      if !qflag then 
+	build_atoms gl metagen false typ 
+      else [] in
+      Left {id=nam;
+	    constr=typ;
+	    pat=pattern;
+	    atoms=l;
+	    internal=internal}
   with Is_atom a-> Right a
-
-let build_right_entry typ metagen=
+    
+let build_right_entry typ gl metagen=
   try
     let pattern=
       match kind_of_formula typ with
@@ -213,8 +239,12 @@ let build_right_entry typ metagen=
 	| Exists (_,d,_,_) -> 
 	    let m=1+(metagen false) in Rexists(m,d) 
 	| Forall (_,a) -> Rforall 
-	| Arrow (a,b) -> Rarrow in
-    let l=build_atoms metagen true typ in
-      Complex(pattern,l)
+	| Arrow (a,b) -> Rarrow 
+	| Evaluable (egc,_)->Revaluable egc in
+    let l=
+      if !qflag then 
+	build_atoms gl metagen true typ
+      else [] in
+      Complex(pattern,typ,l)
   with Is_atom a-> Atomic a
 
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index dfc90a1bf7..1f9d653b2f 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -12,6 +12,10 @@ open Term
 open Names
 open Libnames
 
+val qflag : bool ref
+
+val (+-) : int -> int -> int
+
 type ('a,'b) sum = Left of 'a | Right of 'b
 
 type kind_of_formula=
@@ -21,12 +25,11 @@ type kind_of_formula=
   |Exists of inductive*constr*constr*constr
   |Forall of constr*constr
   |Atom of constr
+  |Evaluable of Names.evaluable_global_reference * Term.constr
   |False
 
 type counter = bool -> int
 
-val newcnt : unit -> counter
-
 val construct_nhyps : inductive -> int array
 
 exception Dependent_Inductive
@@ -35,39 +38,51 @@ val ind_hyps : inductive -> constr list -> Sign.rel_context array
 
 val kind_of_formula : constr -> kind_of_formula
 			
+val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
+  bool -> constr -> (bool*constr) list
+
 type right_pattern =
     Rand
   | Ror 
   | Rforall
   | Rexists of int*constr
   | Rarrow
-      
+  | Revaluable of Names.evaluable_global_reference
+    
 type right_formula =
-    Complex of right_pattern*((bool*constr) list)
+    Complex of right_pattern*constr*((bool*constr) list)
   | Atomic of constr
       
+type left_arrow_pattern=
+    LLatom
+  | LLfalse
+  | LLand of inductive*constr list
+  | LLor of inductive*constr list
+  | LLforall of constr
+  | LLexists of inductive*constr*constr*constr
+  | LLarrow of constr*constr*constr
+  | LLevaluable of Names.evaluable_global_reference
+
 type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
   | Lforall of int*constr
   | Lexists
-  | LAatom of constr
-  | LAfalse
-  | LAand of inductive*constr list
-  | LAor of inductive*constr list
-  | LAforall of constr
-  | LAexists of inductive*constr*constr*constr
-  | LAarrow of constr*constr*constr
+  | Levaluable of Names.evaluable_global_reference
+  | LA of constr*left_arrow_pattern
       
 type left_formula={id:global_reference;
+		   constr:constr;
 		   pat:left_pattern;
 		   atoms:(bool*constr) list;
 		   internal:bool}
 
 val build_left_entry : 
-  global_reference -> types -> bool -> counter -> (left_formula,types) sum
+  global_reference -> types -> bool -> Proof_type.goal Tacmach.sigma ->
+  counter -> (left_formula,types) sum
 
-val build_right_entry : types -> counter -> right_formula
+val build_right_entry : types -> Proof_type.goal Tacmach.sigma -> 
+  counter -> right_formula
 
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 13258818f8..a35896069e 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -22,11 +22,11 @@ open Sequent
 open Unify
 open Libnames
 
-type hptac= Sequent.t -> (Sequent.t -> tactic) -> counter -> tactic
+type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
-type lhptac= global_reference -> hptac
-  
-let wrap n b seq tacrec metagen gls=
+type lseqtac= global_reference -> seqtac
+
+let wrap n b tacrec seq gls=
   let nc=pf_hyps gls in
   let rec aux i nc=
     if i<=0 then seq else 
@@ -34,14 +34,18 @@ let wrap n b seq tacrec metagen gls=
 	  []->anomaly "Not the expected number of hyps"
 	| (id,_,typ)::q-> 
 	    let gr=VarRef id in 
-	    (add_left (gr,typ) (aux (i-1) q) true metagen) in
+	    (add_left (gr,typ) (aux (i-1) q) true gls) in
   let seq1=
     if b then
-      (change_right (pf_concl gls) (aux n nc) metagen)
+      (change_right (pf_concl gls) (aux n nc) gls)
     else
       (aux n nc) in
     tacrec seq1 gls
 
+let id_of_global=function
+    VarRef id->id
+  | _->assert false
+
 let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
@@ -50,57 +54,81 @@ let axiom_tac t seq=
   try exact_no_check (constr_of_reference (find_left t seq)) 
   with Not_found->tclFAIL 0 "No axiom link" 
 
-let and_tac seq tacrec metagen=
-  tclTHEN simplest_split (wrap 0 true seq tacrec metagen)
+let evaluable_tac ec tacrec seq gl=
+  tclTHEN
+    (unfold_in_concl [[1],ec]) 
+    (wrap 0 true tacrec seq) gl
+
+let left_evaluable_tac ec id tacrec seq gl=
+  tclTHENLIST
+    [generalize [constr_of_reference id];
+     clear_global id;
+     intro;
+     (fun gls->
+	let nid=(Tacmach.pf_nth_hyp_id gls 1) in
+	  unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls);
+     wrap 1 false tacrec seq] gl
+    
+let and_tac tacrec seq=
+  tclTHEN simplest_split (wrap 0 true tacrec seq)
 
-let left_and_tac ind id seq tacrec metagen=
+let left_and_tac ind id tacrec seq=
   let n=(construct_nhyps ind).(0) in  
     tclTHENLIST 
       [simplest_elim (constr_of_reference id);
        clear_global id; 
        tclDO n intro;
-       wrap n false seq tacrec metagen]
+       wrap n false tacrec seq]
 
-let or_tac seq tacrec metagen=
-  any_constructor (Some (tclSOLVE [wrap 0 true seq tacrec metagen]))
+let or_tac tacrec seq=
+  any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
 
-let left_or_tac ind id seq tacrec metagen=
+let left_or_tac ind id tacrec seq=
   let v=construct_nhyps ind in  
   let f n=
     tclTHENLIST
       [clear_global id;
        tclDO n intro;
-       wrap n false seq tacrec metagen] in
+       wrap n false tacrec seq] in
     tclTHENSV
       (simplest_elim (constr_of_reference id))
       (Array.map f v)
 
-let forall_tac seq tacrec metagen=
-  tclTHEN intro (wrap 0 true seq tacrec metagen)
+let forall_tac tacrec seq=
+  tclTHEN intro (wrap 0 true tacrec seq)
 
-let left_forall_tac i dom atoms id seq tacrec metagen=
+let left_forall_tac i dom atoms internal id tacrec seq=
   let insts=find_instances i atoms seq in
-    if insts=[] 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 seq tacrec metagen]]
-	;tclIDTAC]
+    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=
-	tclTHENLIST 
-	  [generalize [mkApp(constr_of_reference id,[|t|])];
-	   intro; 
-	   tclSOLVE [wrap 1 false seq tacrec metagen]] in
+	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))]] in
 	tclFIRST (List.map tac insts)
 	  
-let arrow_tac seq tacrec metagen=
-  tclTHEN intro (wrap 1 true seq tacrec metagen)
+let arrow_tac tacrec seq=
+  tclTHEN intro (wrap 1 true tacrec seq)
     
-let exists_tac i dom atoms seq tacrec metagen=
+let exists_tac i dom atoms tacrec seq=
   let insts=find_instances i atoms seq in
     if insts=[] then 
       tclTHENS (cut dom) 
@@ -109,22 +137,22 @@ let exists_tac i dom atoms seq tacrec metagen=
 	    (fun gls->
 	       split (Rawterm.ImplicitBindings 
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
-	       tclSOLVE [wrap 0 false seq tacrec metagen]]
-	    ;tclIDTAC]
+	       tclSOLVE [wrap 0 false tacrec (deepen seq)]]
+	    ;tclTRY assumption]
 	 else
 	   let tac t=
 	     tclTHEN (split (Rawterm.ImplicitBindings [t]))
-	       (tclSOLVE [wrap 0 true seq tacrec metagen]) in
+	       (tclSOLVE [wrap 0 true tacrec (deepen seq)]) in
 	     tclFIRST (List.map tac insts)
 	       
-let left_exists_tac id seq tacrec metagen=
+let left_exists_tac id tacrec seq=
   tclTHENLIST
     [simplest_elim (constr_of_reference id);
      clear_global id;
      tclDO 2 intro;
-     (wrap 1 false seq tacrec metagen)]
+     (wrap 1 false tacrec seq)]
 
-let ll_arrow_tac a b c id seq tacrec metagen=
+let ll_arrow_tac a b c id tacrec seq=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d=mkLambda (Anonymous,b,
 		  mkApp ((constr_of_reference id),
@@ -133,34 +161,34 @@ let ll_arrow_tac a b c id seq tacrec metagen=
       [tclTHENLIST
 	 [intro;
 	  clear_global id;
-	  wrap 1 false seq tacrec metagen];
+	  wrap 1 false tacrec seq];
        tclTHENS (cut cc) 
          [exact_no_check (constr_of_reference id); 
 	  tclTHENLIST 
 	    [generalize [d];
 	     intro;
 	     clear_global id;
-	     tclSOLVE [wrap 1 true seq tacrec metagen]]]]
+	     tclSOLVE [wrap 1 true tacrec seq]]]]
 
-let ll_atom_tac a id seq tacrec metagen=
+let ll_atom_tac a id tacrec seq=
   try 
     tclTHENLIST
       [generalize [mkApp(constr_of_reference id,
 			 [|constr_of_reference (find_left a seq)|])];
        clear_global id;
        intro;
-       wrap 1 false seq tacrec metagen] 
+       wrap 1 false tacrec seq] 
   with Not_found->tclFAIL 0 "No link" 
 
-let ll_false_tac id seq tacrec metagen=
-  tclTHEN (clear_global id) (wrap 0 false seq tacrec metagen)
+let ll_false_tac id tacrec seq=
+  tclTHEN (clear_global id) (wrap 0 false tacrec seq)
 
 let left_false_tac id=
   simplest_elim (constr_of_reference id)
 
 (*We use this function for and, or, exists*)
 
-let ll_ind_tac ind largs id seq tacrec metagen gl= 
+let ll_ind_tac ind largs id tacrec seq gl= 
   (try
      let rcs=ind_hyps ind largs in
      let vargs=Array.of_list largs in
@@ -179,10 +207,10 @@ let ll_ind_tac ind largs id seq tacrec metagen gl=
 	   [generalize newhyps;
 	    clear_global id;
 	    tclDO lp intro;
-	    wrap lp false seq tacrec metagen]
+	    wrap lp false tacrec seq]
    with Dependent_Inductive | Invalid_argument _ ->tclFAIL 0 "") gl
 
-let ll_forall_tac prod id seq tacrec metagen=
+let ll_forall_tac prod id tacrec seq=
   tclTHENS (cut prod)
     [tclTHENLIST
        [(fun gls->generalize 
@@ -190,6 +218,6 @@ let ll_forall_tac prod id seq tacrec metagen=
 		  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 	clear_global id;
 	intro;
-	tclSOLVE [wrap 1 false seq tacrec metagen]];
-       tclSOLVE [wrap 0 true seq tacrec metagen]]
+	tclSOLVE [wrap 1 false tacrec (deepen seq)]];
+       tclSOLVE [wrap 0 true tacrec (deepen seq)]]
 
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index ee224bc54c..7dbd5f556b 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -13,42 +13,46 @@ open Tacmach
 open Names
 open Libnames
 
-type hptac= Sequent.t -> (Sequent.t -> tactic) -> Formula.counter -> tactic
+type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
-type lhptac= global_reference -> hptac
+type lseqtac= global_reference -> seqtac
 
-val wrap : int -> bool -> hptac
+val wrap : int -> bool -> seqtac
 
 val clear_global: global_reference -> tactic
 
 val axiom_tac : constr -> Sequent.t -> tactic
 
-val and_tac : hptac
+val evaluable_tac : evaluable_global_reference -> seqtac
 
-val left_and_tac : inductive -> lhptac
+val left_evaluable_tac : evaluable_global_reference -> lseqtac
 
-val or_tac : hptac
+val and_tac : seqtac
 
-val left_or_tac : inductive -> lhptac
+val left_and_tac : inductive -> lseqtac
 
-val forall_tac : hptac
+val or_tac : seqtac
 
-val left_forall_tac : int -> types -> (bool * constr) list -> lhptac
+val left_or_tac : inductive -> lseqtac
 
-val arrow_tac : hptac
+val forall_tac : seqtac
 
-val exists_tac : int -> types -> (bool * constr) list -> hptac
+val left_forall_tac : int -> types -> (bool * constr) list -> bool -> lseqtac
+
+val arrow_tac : seqtac
+
+val exists_tac : int -> types -> (bool * constr) list -> seqtac
 	       
-val left_exists_tac : lhptac
+val left_exists_tac : lseqtac
 
-val ll_arrow_tac : constr -> constr -> constr -> lhptac
+val ll_arrow_tac : constr -> constr -> constr -> lseqtac
 
-val ll_atom_tac : constr -> lhptac
+val ll_atom_tac : constr -> lseqtac
 
-val ll_false_tac : lhptac
+val ll_false_tac : lseqtac
 
 val left_false_tac : global_reference -> tactic
 
-val ll_ind_tac : inductive -> constr list -> lhptac
+val ll_ind_tac : inductive -> constr list -> lseqtac
 
-val ll_forall_tac : types -> lhptac
+val ll_forall_tac : types -> lseqtac
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index a229d8b86c..40fe19b30f 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -14,29 +14,33 @@ open Formula
 open Tacmach
 open Names
 open Libnames
+open Pp
 
-let priority=function (* pure heuristics, <=0 for non reversible *)
+let newcnt ()=
+  let cnt=ref (-1) in
+    fun b->if b then incr cnt;!cnt
+
+let priority = function (* pure heuristics, <=0 for non reversible *)
       Lfalse             ->1000
     | Land _             ->  90
     | Lor _              ->  40
-    | Lforall (_,_)      -> -20
+    | Lforall (_,_)      -> -30
     | Lexists            ->  60
-    | LAatom _           ->   0
-    | LAfalse            -> 100
-    | LAand (_,_)      ->  80
-    | LAor (_,_)       ->  70
-    | LAforall _         -> -30
-    | LAexists (_,_,_,_) ->  50
-    | LAarrow  (_,_,_)   ->   -10 
-
-
-let right_atomic=function
-    Atomic _->true
-  | Complex (_,_) ->false
-      
+    | Levaluable _       -> 100
+    | LA(_,lap) ->
+	match lap with
+	    LLatom             ->   0
+	  | LLfalse            -> 100
+	  | LLand (_,_)        ->  80
+	  | LLor (_,_)         ->  70
+	  | LLforall _         -> -20
+	  | LLexists (_,_,_,_) ->  50
+	  | LLarrow  (_,_,_)   -> -10 
+	  | LLevaluable _      -> 100
+
 let right_reversible=
   function
-      Rarrow | Rand | Rforall->true
+      Rarrow | Rand | Rforall | Revaluable _ ->true
     | _ ->false
 	
 let left_reversible lpat=(priority lpat)>0
@@ -44,62 +48,127 @@ let left_reversible lpat=(priority lpat)>0
 module OrderedFormula=
 struct
   type t=left_formula
-  let compare e1 e2=(priority e1.pat) - (priority e2.pat)
+  let compare e1 e2=
+	(priority e1.pat) - (priority e2.pat)
 end
 
 module OrderedConstr=
 struct
   type t=constr
-  let compare=Pervasives.compare
+  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
+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)
 end
 
 module CM=Map.Make(OrderedConstr)
 
+module History=Set.Make(Hitem)
+
+let cm_add typ nam cm=
+  try 
+    let l=CM.find typ cm in CM.add typ (nam::l) cm
+  with
+      Not_found->CM.add typ [nam] cm
+	
+let cm_remove typ nam cm=
+  try
+    let l=CM.find typ cm in 
+    let l0=List.filter (fun id->id<>nam) l in
+      match l0 with 
+	  []->CM.remove typ cm
+	| _ ->CM.add typ l0 cm
+      with Not_found ->cm
+
 module HP=Heap.Functional(OrderedFormula)
 
 type t=
-    {hyps:HP.t;hatoms:global_reference CM.t;gl:right_formula}
-
-let add_left (nam,t) seq internal metagen=
-  match build_left_entry nam t internal metagen with
-      Left f->{seq with hyps=HP.add f seq.hyps}
-    | Right t->{seq with hatoms=CM.add t nam seq.hatoms}
+    {redexes:HP.t;
+     context:(global_reference list) CM.t;
+     latoms:constr list;
+     gl:right_formula;
+     cnt:counter;
+     history:History.t;
+     depth:int}
+
+let deepen seq={seq with depth=seq.depth-1}
+ 
+let record id topt seq={seq with history=History.add (id,topt) seq.history}
+
+let lookup id topt seq=History.mem (id,topt) seq.history
+
+let add_left (nam,t) seq internal gl=
+  match build_left_entry nam t internal gl seq.cnt with
+      Left f->{seq with 
+		 redexes=HP.add f seq.redexes;
+		 context=cm_add f.constr nam seq.context}
+    | Right t->{seq with 
+		  context=cm_add t nam seq.context;
+		  latoms=t::seq.latoms}
 
 let re_add_left_list lf seq=
-  {seq with hyps=List.fold_right HP.add lf seq.hyps} 
-
-let change_right t seq metagen=
-  {seq with gl=build_right_entry t metagen}
+  {seq with 
+     redexes=List.fold_right HP.add lf seq.redexes;
+     context=List.fold_right 
+	       (fun f cm->cm_add f.constr f.id cm) lf seq.context}
 
-let find_left t seq=CM.find t seq.hatoms
+let change_right t seq gl=
+  {seq with gl=build_right_entry t gl seq.cnt}
 
-let atomic_right seq= right_atomic seq.gl 
+let find_left t seq=List.hd (CM.find t seq.context)
 
 let rev_left seq=
   try
-    let lpat=(HP.maximum seq.hyps).pat in
+    let lpat=(HP.maximum seq.redexes).pat in
       left_reversible lpat
   with Heap.EmptyHeap -> false
 
 let is_empty_left seq=
-  seq.hyps=HP.empty
+  seq.redexes=HP.empty
 
 let take_left seq=
-  let hd=HP.maximum seq.hyps
-  and hp=HP.remove seq.hyps in
-    hd,{seq with hyps=hp}
+  let hd=HP.maximum seq.redexes
+  and hp=HP.remove seq.redexes in
+    hd,{seq with 
+	  redexes=hp;
+	  context=cm_remove hd.constr hd.id seq.context}
 
 let take_right seq=seq.gl
 
-let empty_seq=
-  {hyps=HP.empty;
-   hatoms=CM.empty;
-   gl=Atomic (mkMeta 1)}
+let empty_seq depth=
+  {redexes=HP.empty;   
+   context=CM.empty;
+   latoms=[];
+   gl=Atomic (mkMeta 1);
+   cnt=newcnt ();
+   history=History.empty;
+   depth=depth}
+
+let create_with_ref_list l depth gl=
+  let f gr seq=
+    let c=constr_of_reference gr in    
+    let typ=(pf_type_of gl c) in
+      add_left (gr,typ) seq false gl in
+    List.fold_right f l (empty_seq depth)
 
 open Auto
 
-let create_with_auto_hints gl metagen=
-  let seqref=ref empty_seq in
+let create_with_auto_hints depth gl=
+  let seqref=ref (empty_seq depth) in
   let f p_a_t =
     match p_a_t.code with
 	Res_pf (c,_) | Give_exact c
@@ -107,7 +176,7 @@ let create_with_auto_hints gl metagen=
 	  (try 
 	     let gr=reference_of_constr c in 
 	     let typ=(pf_type_of gl c) in
-	       seqref:=add_left (gr,typ) !seqref false metagen
+	       seqref:=add_left (gr,typ) !seqref false gl
 	   with Not_found->())
       | _-> () in
   let g _ l=List.iter f l in
@@ -115,5 +184,20 @@ let create_with_auto_hints gl metagen=
     Util.Stringmap.iter h (!searchtable);
     !seqref
 
+let print_cmap map=
+  
+  let print_entry c l s=
+    let xc=Constrextern.extern_constr false (Global.env ()) c in
+      str "| " ++ 
+      Util.prlist (Ppconstr.pr_global Idset.empty) l ++ 
+      str " : " ++
+      Ppconstr.pr_constr xc ++ 
+      cut () ++ 
+      s in
+    msgnl (v 0 
+	     (str "-----" ++ 
+	      cut () ++
+	      CM.fold print_entry map (mt ()) ++
+	      str "-----"))
 
 	
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index 6b955adac4..751c297453 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -21,15 +21,36 @@ val left_reversible : left_pattern -> bool
 
 module CM: Map.S with type key=constr
 
+module History: Set.S with type elt = global_reference * constr option
+
+val cm_add : constr -> global_reference -> global_reference list CM.t ->
+  global_reference list CM.t
+
+val cm_remove : constr -> global_reference -> global_reference list CM.t ->
+  global_reference list CM.t
+
 module HP: Heap.S with type elt=left_formula
 
-type t = {hyps:HP.t;hatoms: global_reference CM.t;gl:right_formula}
+type t = {redexes:HP.t;
+	  context: global_reference list CM.t;
+	  latoms:constr list;
+	  gl:right_formula;
+	  cnt:counter;
+	  history:History.t;
+	  depth:int}
+
+val deepen: t -> t
 
-val add_left : global_reference * constr -> t -> bool -> counter -> t
+val record: global_reference -> constr option -> t -> t
+
+val lookup: global_reference -> constr option -> t -> bool
+
+val add_left : global_reference * constr -> t -> bool -> 
+  Proof_type.goal sigma -> t
 
 val re_add_left_list : left_formula list -> t -> t
 
-val change_right : constr -> t -> counter -> t
+val change_right : constr -> t -> Proof_type.goal sigma -> t
 
 val find_left : constr -> t -> global_reference
 
@@ -41,6 +62,11 @@ val take_left : t -> left_formula * t
 
 val take_right : t -> right_formula
 
-val empty_seq : t
+val empty_seq : int -> t
+
+val create_with_ref_list : global_reference list ->
+  int -> Proof_type.goal sigma -> t
+
+val create_with_auto_hints : int -> Proof_type.goal sigma -> t
 
-val create_with_auto_hints : Proof_type.goal sigma -> counter -> t
+val print_cmap: global_reference list CM.t -> unit 
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 8dc0d96e6b..0c336b6d31 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -90,20 +90,34 @@ let collect i l=
       if is_ground t then Some t else None
   with Not_found->None
 
+let value i=
+  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
+
+let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
+
 let unif_atoms_for_meta i (b1,t1) (b2,t2)=
-  if b1=b2 then None else
+  if b1=b2  || is_head_meta t1 || is_head_meta t2  then None else
     try 
-      collect i (unif t1 t2) 
+       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=
 struct
-  type t=constr
-  let compare=Pervasives.compare
+  type t=int*constr
+  let compare (n1,t1) (n2,t2)=
+    (n2 - n1) +- (Pervasives.compare t1 t2) 
+    (* we want a decreasing total order *)
 end
-
+  
 module CS=Set.Make(OrderedConstr)
-
+  
 let match_atom_list i atom l=
   let f atom2 accu=
     match unif_atoms_for_meta i atom atom2 with
@@ -118,14 +132,19 @@ let match_lists i l1 l2=
       
 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 nam 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=CM.fold match_atom seq.hatoms s1 in
-  let s3=HP.fold match_hyp seq.hyps s2 in
-    CS.fold (fun x l->x::l) s3 []
+      | 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)
 
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 04d7951014..5423884886 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -10,4 +10,7 @@
 
 open Term
 
+val unif_atoms_for_meta : int -> (bool * constr) -> (bool * constr) ->
+  (int*constr) option
+
 val find_instances : int -> (bool * constr) list -> Sequent.t -> constr list
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ff735c9cd5..98976a91c5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -204,12 +204,13 @@ let match_with_nodep_ind t =
   match (kind_of_term hdapp) with
     | Ind ind  -> 
         let (mib,mip) = Global.lookup_inductive ind in
-        let constr_types = mip.mind_nf_lc in 
-	let nodep_constr = has_nodep_prod_after mip.mind_nparams in	
-	if array_for_all nodep_constr constr_types then 
-	  Some (hdapp,args)
-        else 
-	  None
+          if mip.mind_nrealargs>0 then None else
+	    let constr_types = mip.mind_nf_lc in 
+	    let nodep_constr = has_nodep_prod_after mip.mind_nparams in	
+	      if array_for_all nodep_constr constr_types then 
+		Some (hdapp,args)
+              else 
+		None
     | _ -> None
 	  
 let is_nodep_ind t=op2bool (match_with_nodep_ind t)