Report de l'heuristique d'unification premier ordre flexible/rigide

en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
  de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)


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

10 files changed, 230 insertions, 231 deletions

diff --git a/.depend b/.depend
index 46b3ece083..5a1dec9897 100644
--- a/.depend
+++ b/.depend
@@ -490,7 +490,7 @@ contrib/subtac/subtac_pretyping.cmi: interp/topconstr.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/pretyping.cmi kernel/names.cmi \
     library/global.cmi pretyping/evd.cmi kernel/environ.cmi 
 contrib/subtac/subtac_utils.cmi: lib/util.cmi interp/topconstr.cmi \
-    kernel/term.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
+    kernel/term.cmi proofs/tacexpr.cmo kernel/sign.cmi pretyping/rawterm.cmi \
     proofs/proof_type.cmi lib/pp.cmi kernel/names.cmi library/libnames.cmi \
     pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
     library/decl_kinds.cmo interp/coqlib.cmi 
@@ -1011,8 +1011,6 @@ library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi
 library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi 
 lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
 lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
 lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
 lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
 lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
@@ -1363,16 +1361,18 @@ pretyping/detyping.cmx: lib/util.cmx kernel/univ.cmx pretyping/termops.cmx \
     kernel/inductive.cmx library/goptions.cmx library/global.cmx \
     pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \
     pretyping/detyping.cmi 
-pretyping/evarconv.cmo: lib/util.cmi pretyping/typing.cmi kernel/term.cmi \
-    pretyping/reductionops.cmi kernel/reduction.cmi pretyping/recordops.cmi \
-    kernel/names.cmi library/libnames.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi kernel/environ.cmi kernel/closure.cmi \
-    pretyping/classops.cmi pretyping/evarconv.cmi 
-pretyping/evarconv.cmx: lib/util.cmx pretyping/typing.cmx kernel/term.cmx \
-    pretyping/reductionops.cmx kernel/reduction.cmx pretyping/recordops.cmx \
-    kernel/names.cmx library/libnames.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx kernel/environ.cmx kernel/closure.cmx \
-    pretyping/classops.cmx pretyping/evarconv.cmi 
+pretyping/evarconv.cmo: lib/util.cmi pretyping/typing.cmi \
+    pretyping/termops.cmi kernel/term.cmi pretyping/reductionops.cmi \
+    kernel/reduction.cmi pretyping/recordops.cmi lib/pp.cmi kernel/names.cmi \
+    library/libnames.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    kernel/environ.cmi kernel/closure.cmi pretyping/classops.cmi \
+    pretyping/evarconv.cmi 
+pretyping/evarconv.cmx: lib/util.cmx pretyping/typing.cmx \
+    pretyping/termops.cmx kernel/term.cmx pretyping/reductionops.cmx \
+    kernel/reduction.cmx pretyping/recordops.cmx lib/pp.cmx kernel/names.cmx \
+    library/libnames.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    kernel/environ.cmx kernel/closure.cmx pretyping/classops.cmx \
+    pretyping/evarconv.cmi 
 pretyping/evarutil.cmo: lib/util.cmi kernel/univ.cmi pretyping/typing.cmi \
     kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \
     pretyping/reductionops.cmi kernel/reduction.cmi \
@@ -2119,6 +2119,8 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
     pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \
     library/nameops.cmx library/libnames.cmx tactics/dn.cmx \
     tactics/termdn.cmi 
+test-suite/zarith.cmo: test-suite/zarith.cmi 
+test-suite/zarith.cmx: test-suite/zarith.cmi 
 tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi 
 tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
@@ -2154,33 +2156,35 @@ toplevel/class.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
 toplevel/command.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/typeops.cmi \
     interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
     proofs/tacmach.cmi interp/syntax_def.cmi library/states.cmi \
-    kernel/safe_typing.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
-    kernel/reduction.cmi proofs/redexpr.cmi pretyping/rawterm.cmi \
-    proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \
+    kernel/sign.cmi kernel/safe_typing.cmi pretyping/retyping.cmi \
+    pretyping/reductionops.cmi kernel/reduction.cmi proofs/redexpr.cmi \
+    pretyping/rawterm.cmi proofs/proof_type.cmi pretyping/pretyping.cmi \
     lib/pp.cmi proofs/pfedit.cmi lib/options.cmi interp/notation.cmi \
     library/nametab.cmi kernel/names.cmi library/nameops.cmi \
     toplevel/metasyntax.cmi proofs/logic.cmi library/library.cmi \
     library/libobject.cmi library/libnames.cmi library/lib.cmi \
     kernel/inductive.cmi kernel/indtypes.cmi pretyping/indrec.cmi \
     library/impargs.cmi library/global.cmi pretyping/evd.cmi \
-    kernel/environ.cmi kernel/entries.cmi library/declare.cmi \
-    kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \
-    interp/constrextern.cmi toplevel/class.cmi toplevel/command.cmi 
+    pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
+    kernel/entries.cmi library/declare.cmi kernel/declarations.cmi \
+    library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \
+    toplevel/class.cmi toplevel/command.cmi 
 toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \
     interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
     proofs/tacmach.cmx interp/syntax_def.cmx library/states.cmx \
-    kernel/safe_typing.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \
-    kernel/reduction.cmx proofs/redexpr.cmx pretyping/rawterm.cmx \
-    proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \
+    kernel/sign.cmx kernel/safe_typing.cmx pretyping/retyping.cmx \
+    pretyping/reductionops.cmx kernel/reduction.cmx proofs/redexpr.cmx \
+    pretyping/rawterm.cmx proofs/proof_type.cmx pretyping/pretyping.cmx \
     lib/pp.cmx proofs/pfedit.cmx lib/options.cmx interp/notation.cmx \
     library/nametab.cmx kernel/names.cmx library/nameops.cmx \
     toplevel/metasyntax.cmx proofs/logic.cmx library/library.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
     kernel/inductive.cmx kernel/indtypes.cmx pretyping/indrec.cmx \
     library/impargs.cmx library/global.cmx pretyping/evd.cmx \
-    kernel/environ.cmx kernel/entries.cmx library/declare.cmx \
-    kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \
-    interp/constrextern.cmx toplevel/class.cmx toplevel/command.cmi 
+    pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
+    kernel/entries.cmx library/declare.cmx kernel/declarations.cmx \
+    library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \
+    toplevel/class.cmx toplevel/command.cmi 
 toplevel/coqinit.cmo: toplevel/vernac.cmi toplevel/toplevel.cmi \
     lib/system.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \
     library/nameops.cmi toplevel/mltop.cmi config/coq_config.cmi \
@@ -3544,15 +3548,15 @@ contrib/subtac/context.cmo: kernel/term.cmi kernel/names.cmi \
 contrib/subtac/context.cmx: kernel/term.cmx kernel/names.cmx \
     contrib/subtac/context.cmi 
 contrib/subtac/eterm.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
-    tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi lib/pp.cmi \
-    lib/options.cmi kernel/names.cmi library/global.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi kernel/environ.cmi library/declare.cmi \
-    library/decl_kinds.cmo contrib/subtac/eterm.cmi 
+    tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
+    parsing/printer.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    kernel/environ.cmi contrib/subtac/eterm.cmi 
 contrib/subtac/eterm.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
-    tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx lib/pp.cmx \
-    lib/options.cmx kernel/names.cmx library/global.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx kernel/environ.cmx library/declare.cmx \
-    library/decl_kinds.cmx contrib/subtac/eterm.cmi 
+    tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \
+    parsing/printer.cmx lib/pp.cmx lib/options.cmx kernel/names.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    kernel/environ.cmx contrib/subtac/eterm.cmi 
 contrib/subtac/g_eterm.cmo: lib/util.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
     parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi contrib/subtac/eterm.cmi \
@@ -3564,17 +3568,17 @@ contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \
 contrib/subtac/g_subtac.cmo: toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo toplevel/vernacentries.cmi lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \
-    contrib/subtac/subtac.cmi kernel/reduction.cmi proofs/proof_type.cmi \
-    lib/pp.cmi parsing/pcoq.cmi lib/options.cmi kernel/names.cmi \
-    library/nameops.cmi library/libnames.cmi interp/genarg.cmi \
-    parsing/egrammar.cmi toplevel/cerrors.cmi 
+    contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac.cmi \
+    kernel/reduction.cmi proofs/proof_type.cmi lib/pp.cmi parsing/pcoq.cmi \
+    lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+    interp/genarg.cmi parsing/egrammar.cmi toplevel/cerrors.cmi 
 contrib/subtac/g_subtac.cmx: toplevel/vernacinterp.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacentries.cmx lib/util.cmx \
     interp/topconstr.cmx kernel/term.cmx proofs/tacexpr.cmx \
-    contrib/subtac/subtac.cmx kernel/reduction.cmx proofs/proof_type.cmx \
-    lib/pp.cmx parsing/pcoq.cmx lib/options.cmx kernel/names.cmx \
-    library/nameops.cmx library/libnames.cmx interp/genarg.cmx \
-    parsing/egrammar.cmx toplevel/cerrors.cmx 
+    contrib/subtac/subtac_obligations.cmx contrib/subtac/subtac.cmx \
+    kernel/reduction.cmx proofs/proof_type.cmx lib/pp.cmx parsing/pcoq.cmx \
+    lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+    interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx 
 contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
     pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
     contrib/subtac/subtac_errors.cmi pretyping/retyping.cmi \
@@ -3599,40 +3603,42 @@ contrib/subtac/subtac_command.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo interp/syntax_def.cmi \
     contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \
-    library/states.cmi kernel/sign.cmi kernel/safe_typing.cmi \
-    interp/reserve.cmi proofs/refiner.cmi pretyping/reductionops.cmi \
-    pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
-    pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \
-    pretyping/pattern.cmi lib/options.cmi interp/notation.cmi \
-    library/nametab.cmi kernel/names.cmi library/nameops.cmi \
-    kernel/mod_subst.cmi toplevel/metasyntax.cmi pretyping/matching.cmi \
-    library/libobject.cmi library/libnames.cmi pretyping/inductiveops.cmi \
-    library/impargs.cmi tactics/hiddentac.cmi library/global.cmi \
-    interp/genarg.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
-    contrib/subtac/eterm.cmi kernel/environ.cmi kernel/entries.cmi \
-    lib/dyn.cmi library/declare.cmi kernel/declarations.cmi \
-    library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \
-    toplevel/command.cmi kernel/closure.cmi contrib/subtac/subtac_command.cmi 
+    contrib/subtac/subtac_obligations.cmo library/states.cmi kernel/sign.cmi \
+    kernel/safe_typing.cmi interp/reserve.cmi proofs/refiner.cmi \
+    pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
+    parsing/printer.cmi pretyping/pretyping.cmi parsing/ppconstr.cmi \
+    lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi lib/options.cmi \
+    interp/notation.cmi library/nametab.cmi kernel/names.cmi \
+    library/nameops.cmi kernel/mod_subst.cmi toplevel/metasyntax.cmi \
+    pretyping/matching.cmi library/libobject.cmi library/libnames.cmi \
+    pretyping/inductiveops.cmi library/impargs.cmi tactics/hiddentac.cmi \
+    library/global.cmi interp/genarg.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
+    kernel/entries.cmi lib/dyn.cmi library/declare.cmi \
+    kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+    interp/constrintern.cmi toplevel/command.cmi kernel/closure.cmi \
+    contrib/subtac/subtac_command.cmi 
 contrib/subtac/subtac_command.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     pretyping/typing.cmx interp/topconstr.cmx pretyping/termops.cmx \
     kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
     proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx interp/syntax_def.cmx \
     contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \
-    library/states.cmx kernel/sign.cmx kernel/safe_typing.cmx \
-    interp/reserve.cmx proofs/refiner.cmx pretyping/reductionops.cmx \
-    pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
-    pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \
-    pretyping/pattern.cmx lib/options.cmx interp/notation.cmx \
-    library/nametab.cmx kernel/names.cmx library/nameops.cmx \
-    kernel/mod_subst.cmx toplevel/metasyntax.cmx pretyping/matching.cmx \
-    library/libobject.cmx library/libnames.cmx pretyping/inductiveops.cmx \
-    library/impargs.cmx tactics/hiddentac.cmx library/global.cmx \
-    interp/genarg.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
-    contrib/subtac/eterm.cmx kernel/environ.cmx kernel/entries.cmx \
-    lib/dyn.cmx library/declare.cmx kernel/declarations.cmx \
-    library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \
-    toplevel/command.cmx kernel/closure.cmx contrib/subtac/subtac_command.cmi 
+    contrib/subtac/subtac_obligations.cmx library/states.cmx kernel/sign.cmx \
+    kernel/safe_typing.cmx interp/reserve.cmx proofs/refiner.cmx \
+    pretyping/reductionops.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \
+    parsing/printer.cmx pretyping/pretyping.cmx parsing/ppconstr.cmx \
+    lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx lib/options.cmx \
+    interp/notation.cmx library/nametab.cmx kernel/names.cmx \
+    library/nameops.cmx kernel/mod_subst.cmx toplevel/metasyntax.cmx \
+    pretyping/matching.cmx library/libobject.cmx library/libnames.cmx \
+    pretyping/inductiveops.cmx library/impargs.cmx tactics/hiddentac.cmx \
+    library/global.cmx interp/genarg.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
+    kernel/entries.cmx lib/dyn.cmx library/declare.cmx \
+    kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+    interp/constrintern.cmx toplevel/command.cmx kernel/closure.cmx \
+    contrib/subtac/subtac_command.cmi 
 contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi \
     contrib/subtac/subtac_errors.cmi 
 contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx \
@@ -3691,6 +3697,16 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     lib/dyn.cmx library/decl_kinds.cmx interp/coqlib.cmx \
     contrib/subtac/context.cmx toplevel/command.cmx pretyping/classops.cmx \
     toplevel/cerrors.cmx contrib/subtac/subtac.cmi 
+contrib/subtac/subtac_obligations.cmo: lib/util.cmi kernel/term.cmi \
+    library/summary.cmi contrib/subtac/subtac_utils.cmi lib/pp.cmi \
+    kernel/names.cmi library/libobject.cmi library/libnames.cmi \
+    kernel/entries.cmi library/declare.cmi library/decl_kinds.cmo \
+    toplevel/command.cmi 
+contrib/subtac/subtac_obligations.cmx: lib/util.cmx kernel/term.cmx \
+    library/summary.cmx contrib/subtac/subtac_utils.cmx lib/pp.cmx \
+    kernel/names.cmx library/libobject.cmx library/libnames.cmx \
+    kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \
+    toplevel/command.cmx 
 contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
@@ -3714,7 +3730,8 @@ contrib/subtac/subtac_pretyping_F.cmx: lib/util.cmx kernel/typeops.cmx \
 contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi kernel/type_errors.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
-    contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_errors.cmi \
+    contrib/subtac/subtac_pretyping_F.cmo \
+    contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_errors.cmi \
     contrib/subtac/subtac_coercion.cmi kernel/sign.cmi \
     pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \
     parsing/printer.cmi pretyping/pretype_errors.cmi lib/pp.cmi \
@@ -3727,7 +3744,8 @@ contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
 contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     kernel/typeops.cmx kernel/type_errors.cmx interp/topconstr.cmx \
     pretyping/termops.cmx kernel/term.cmx contrib/subtac/subtac_utils.cmx \
-    contrib/subtac/subtac_pretyping_F.cmx contrib/subtac/subtac_errors.cmx \
+    contrib/subtac/subtac_pretyping_F.cmx \
+    contrib/subtac/subtac_obligations.cmx contrib/subtac/subtac_errors.cmx \
     contrib/subtac/subtac_coercion.cmx kernel/sign.cmx \
     pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \
     parsing/printer.cmx pretyping/pretype_errors.cmx lib/pp.cmx \
@@ -3857,6 +3875,10 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
 contrib/xml/xml.cmo: contrib/xml/xml.cmi 
 contrib/xml/xml.cmx: contrib/xml/xml.cmi 
+doc/refman/euclid.cmo: doc/refman/euclid.cmi 
+doc/refman/euclid.cmx: doc/refman/euclid.cmi 
+doc/refman/heapsort.cmo: doc/refman/heapsort.cmi 
+doc/refman/heapsort.cmx: doc/refman/heapsort.cmi 
 ide/utils/config_file.cmo: ide/utils/config_file.cmi 
 ide/utils/config_file.cmx: ide/utils/config_file.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \
@@ -4010,94 +4032,72 @@ tools/coq-tex.cmx:
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
   /usr/local/lib/ocaml/caml/config.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   /usr/local/lib/ocaml/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
   /usr/local/lib/ocaml/caml/config.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   /usr/local/lib/ocaml/caml/alloc.h
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 7bfaa0c5c5..afbc56f68c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -557,35 +557,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
       nf_evar (evars_of !isevars) c'
 
-  (* [check_evars] fails if some unresolved evar remains *)
-  (* it assumes that the defined existentials have already been substituted
-     (should be done in unsafe_infer and unsafe_infer_type) *)
-
-  let check_evars env initial_sigma isevars c =
-    let sigma = evars_of !isevars in
-    let rec proc_rec c =
-      match kind_of_term c with
-	| Evar (ev,args) ->
-            assert (Evd.mem sigma ev);
-	    if not (Evd.mem initial_sigma ev) then
-              let (loc,k) = evar_source ev !isevars in
-		error_unsolvable_implicit loc env sigma k
-	| _ -> iter_constr proc_rec c
-    in
-      proc_rec c(*;
-		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-		  if pbs <> [] then begin
-		  pperrnl
-		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-		  prlist_with_sep fnl
-		  (fun  (pb,c1,c2) ->
-		  Termops.print_constr c1 ++
-		  (if pb=Reduction.CUMUL then str " <="++ spc()
-		  else str" =="++spc()) ++
-		  Termops.print_constr c2)
-		  pbs ++ fnl())
-		  end*)
-
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -595,6 +566,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
     let j = j_nf_evar (evars_of !isevars) j in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
@@ -611,8 +583,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let c = nf_evar (evars_of isevars) c in
       if fail_evar then check_evars env sigma isevars c;
-      !isevars, c
+      isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 48da52bb25..34f5a3c14f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -191,12 +191,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   else 
     let (t1,l1) = apprec_nohdbeta env isevars term1 in
     let (t2,l2) = apprec_nohdbeta env isevars term2 in
-    if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
-      or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
-    then 
-      (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
-    else 
-      evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+    evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
@@ -235,13 +230,15 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    not (occur_evar (fst ev1) (applist (term2,l2)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
 	    solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
 	  then
-	  (* Try first-order unification *)
+	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
 	    let (deb2,rest2) =
               list_chop (List.length l2-List.length l1) l2 in
             ise_and i
@@ -265,6 +262,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    not (occur_evar (fst ev2) (applist (term1,l1)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
@@ -272,6 +270,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
        	    List.length l2 <= List.length l1
 	  then
 	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
             (* First compare extra args for better failure message *)
@@ -322,25 +321,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  not (occur_evar (fst ev1) (applist (term2,l2)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
-	else if
-       	  List.length l1 <= List.length l2
-	then
-	  (* Try first-order unification *)
-       	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-          ise_and isevars
-            (* First compare extra args for better failure message *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
-             (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t2 = applist(term2,deb2) in
-	       if is_defined_evar i ev1 then
-		 evar_conv_x env i pbty (mkEvar ev1) t2
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
-        else (isevars,false)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
 
     | Rigid _, Flexible ev2 ->
 	if 
@@ -348,25 +336,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  not (occur_evar (fst ev2) (applist (term1,l1)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
-	else if
-	  List.length l2 <= List.length l1
-	then
-	  (* Try first-order unification *)
-       	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-          ise_and isevars
-            (* First compare extra args for better failure message *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
-	     (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t1 = applist(term1,deb1) in
-	       if is_defined_evar i ev2 then
-		 evar_conv_x env i pbty t1 (mkEvar ev2)
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
-        else (isevars,false)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
 
     | MaybeFlexible flex1, Rigid _ ->
 	let f3 i =
@@ -514,6 +491,50 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
      (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
      (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
 
+let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+  match kind_of_term term1, kind_of_term term2 with
+    | Evar ev1,_ when List.length l1 <= List.length l2 ->
+	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t2 = applist(term2,deb2) in
+	  if is_defined_evar i ev1 then
+	    evar_conv_x env i pbty t2 (mkEvar ev1)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
+    | _,Evar ev2 when List.length l2 <= List.length l1 ->
+	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t1 = applist(term1,deb1) in
+	  if is_defined_evar i ev2 then
+	    evar_conv_x env i pbty t1 (mkEvar ev2)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
+    | _ -> 
+	(* Some head evar have been instantiated *)
+	evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+
+let consider_remaining_unif_problems env isevars =
+  let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+  List.fold_left
+    (fun (isevars,b as p) (pbty,t1,t2) ->
+      (* Pas le bon env pour le problème... *)
+      if b then first_order_unification env isevars pbty 
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+      else p)
+    (isevars,true)
+    pbs
+
+(* Main entry points *)
+
 let the_conv_x     env t1 t2 isevars =
   match evar_conv_x env isevars CONV  t1 t2 with
       (evd',true) -> evd'
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 41b5e05fa1..538ac29b9e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -33,3 +33,5 @@ val evar_eqappr_x :
     conv_pb -> constr * constr list -> constr * constr list ->
       evar_defs * bool
 (*i*)
+
+val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 47b10e6dd0..262214c3a7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -603,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
       (fun (isevars,b as p) (pbty,t1,t2) ->
-        if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
     (isevars,false)
 
+
+(* [check_evars] fails if some unresolved evar remains *)
+(* it assumes that the defined existentials have already been substituted *)
+
+let check_evars env initial_sigma isevars c =
+  let sigma = evars_of isevars in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (ev,args) ->
+          assert (Evd.mem sigma ev);
+	  if not (Evd.mem initial_sigma ev) then
+            let (loc,k) = evar_source ev isevars in
+	    error_unsolvable_implicit loc env sigma k
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 98db6174f6..670b742707 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -78,6 +78,10 @@ val solve_simple_eqn :
   -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
+(* [check_evars env initial_sigma extended_sigma c] fails if some
+   new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_defs -> constr -> unit
+
 val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
 val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 738a951470..bb973b71ee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -114,8 +114,6 @@ sig
 
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-  val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit
-
   (*i*)
   (* Internal of Pretyping...
    * Unused outside, but useful for debugging
@@ -634,35 +632,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
       nf_evar (evars_of !isevars) c'
 
-  (* [check_evars] fails if some unresolved evar remains *)
-  (* it assumes that the defined existentials have already been substituted
-     (should be done in unsafe_infer and unsafe_infer_type) *)
-
-  let check_evars env initial_sigma isevars c =
-    let sigma = evars_of !isevars in
-    let rec proc_rec c =
-      match kind_of_term c with
-	| Evar (ev,args) ->
-            assert (Evd.mem sigma ev);
-	    if not (Evd.mem initial_sigma ev) then
-              let (loc,k) = evar_source ev !isevars in
-		error_unsolvable_implicit loc env sigma k
-	| _ -> iter_constr proc_rec c
-    in
-      proc_rec c(*;
-		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-		  if pbs <> [] then begin
-		  pperrnl
-		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-		  prlist_with_sep fnl
-		  (fun  (pb,c1,c2) ->
-		  Termops.print_constr c1 ++
-		  (if pb=Reduction.CUMUL then str " <="++ spc()
-		  else str" =="++spc()) ++
-		  Termops.print_constr c2)
-		  pbs ++ fnl())
-		  end*)
-
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -671,7 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let j = j_nf_evar (evars_of !isevars) j in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let j = j_nf_evar (evars_of isevars) j in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
@@ -688,8 +658,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let c = nf_evar (evars_of isevars) c in
       if fail_evar then check_evars env sigma isevars c;
-      !isevars, c
+      isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 06b290b1da..0b9b47b7a7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -78,8 +78,6 @@ sig
   (* Idem but do not fail on unresolved evars *)
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-  val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit
-       
   (*i*)
   (* Internal of Pretyping...
    *)
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index baeec14781..ad69ced19e 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -68,3 +68,9 @@ Proof. trivial. Qed.
 Hint Resolve contradiction.
 Goal False.
 eauto.
+
+(* This used to fail in V8.1beta because first-order unification was
+   used before using type information *)
+
+Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
+Check (exist _ O I : {n:nat|True}).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4d8e48c795..b333a51bb4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -39,7 +39,8 @@ open Indtypes
 open Vernacexpr
 open Decl_kinds
 open Pretyping
-open Pretyping.Default
+open Evarutil
+open Evarconv
 open Notation
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
@@ -338,7 +339,9 @@ let interp_mutual paramsl indl notations finite =
      () in
 
   (* Instantiate evars and check all are resolved *)
-  let sigma = Evd.evars_of !isevars in
+  let isevars,_ = consider_remaining_unif_problems env_params !isevars in
+  let sigma = Evd.evars_of isevars in
+  let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
   List.iter (check_evars env_params Evd.empty isevars) arities;
@@ -580,7 +583,9 @@ let interp_recursive fixkind l boxed =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let fixtypes = List.map (nf_evar (Evd.evars_of !isevars)) fixtypes in
+  let isevars,_ = consider_remaining_unif_problems env_rec !isevars in
+  let fixdefs = List.map (nf_evar (Evd.evars_of isevars)) fixdefs in
+  let fixtypes = List.map (nf_evar (Evd.evars_of isevars)) fixtypes in
   List.iter (check_evars env_rec Evd.empty isevars) fixdefs;
   check_mutuality env kind (List.combine fixnames fixdefs);