Merge branch 'v8.5'

40 files changed, 828 insertions, 274 deletions

diff --git a/CHANGES b/CHANGES
index 19da2a4c81..712a8a7e92 100644
--- a/CHANGES
+++ b/CHANGES
@@ -260,6 +260,12 @@ Tactics
     an inductive type with indices is fixed
   - residual local definitions are now correctly removed.
 - The rename tactic may now replace variables in parallel.
+- A new "Info" command replaces the "info" tactical discontinued in
+  v8.4. It still gives informative results in many cases.
+- The "info_auto" tactic is known to be broken and does not print a
+  trace anymore. Use "Info 1 auto" instead. The same goes for
+  "info_trivial". On the other hand "info_eauto" still works fine,
+  while "Info 1 eauto" prints a trivial trace.
 
 Program
 
diff --git a/Makefile b/Makefile
index c7fb1ff768..554718bc77 100644
--- a/Makefile
+++ b/Makefile
@@ -169,7 +169,7 @@ Makefile Makefile.build Makefile.common config/Makefile : ;
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean doclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
 
 clean: objclean cruftclean depclean docclean devdocclean
 
diff --git a/checker/cic.mli b/checker/cic.mli
index a793fefa83..90a0e9feb6 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -333,7 +333,7 @@ type ('ty,'a) functorize =
 
 type with_declaration =
   | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * constr
+  | WithDef of Id.t list * (constr * Univ.universe_context)
 
 type module_alg_expr =
   | MEident of module_path
diff --git a/checker/declarations.ml b/checker/declarations.ml
index c6709a7852..8d913475f9 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -583,7 +583,7 @@ let implem_map fs fa = function
 
 let subst_with_body sub = function
   | WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
-  | WithDef(id,c) -> WithDef(id,subst_mps sub c)
+  | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx))
 
 let rec subst_expr sub = function
   | MEident mp -> MEident (subst_mp sub mp)
diff --git a/checker/values.ml b/checker/values.ml
index 3ca44b7d0f..c986415070 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli
+MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
 
 *)
 
@@ -270,7 +270,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
 let v_with =
   Sum ("with_declaration_body",0,
        [|[|List v_id;v_mp|];
-         [|List v_id;v_constr|]|])
+         [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|])
 
 let rec v_mae =
   Sum ("module_alg_expr",0,
diff --git a/configure.ml b/configure.ml
index fbfd8833b9..e83ebc7afd 100644
--- a/configure.ml
+++ b/configure.ml
@@ -245,7 +245,7 @@ module Prefs = struct
   let coqide = ref (None : ide option)
   let macintegration = ref true
   let browser = ref (None : string option)
-  let withdoc = ref true
+  let withdoc = ref false
   let geoproof = ref false
   let byteonly = ref false
   let debug = ref false
@@ -291,7 +291,7 @@ let args_options = Arg.align [
   "-coqdocdir", arg_string_option Prefs.coqdocdir,
     "<dir> Where to install Coqdoc style files";
   "-camldir", arg_string_option Prefs.camldir,
-    "<dir> Specifies the path to the OCaml library";
+    "<dir> Specifies the path to the OCaml binaries";
   "-lablgtkdir", arg_string_option Prefs.lablgtkdir,
     "<dir> Specifies the path to the Lablgtk library";
   "-usecamlp5", Arg.Set Prefs.usecamlp5,
@@ -359,8 +359,7 @@ type camlexec =
    mutable dep : string;
    mutable doc : string;
    mutable lex : string;
-   mutable yacc : string;
-   mutable p4 : string }
+   mutable yacc : string }
 
 (* TODO: autodetect .opt binaries ? *)
 
@@ -372,8 +371,7 @@ let camlexec =
     dep = "ocamldep";
     doc = "ocamldoc";
     lex = "ocamllex";
-    yacc = "ocamlyacc";
-    p4 = "camlp4o" }
+    yacc = "ocamlyacc" }
 
 let reset_caml_byte c o = c.byte <- o
 let reset_caml_opt c o = c.opt <- o
@@ -389,8 +387,7 @@ let rebase_camlexec dir c =
   c.dep <- Filename.concat dir c.dep;
   c.doc <- Filename.concat dir c.doc;
   c.lex <- Filename.concat dir c.lex;
-  c.yacc <- Filename.concat dir c.yacc;
-  c.p4 <- Filename.concat dir c.p4
+  c.yacc <- Filename.concat dir c.yacc
 
 let coq_debug_flag = if !Prefs.debug then "-g" else ""
 let coq_profile_flag = if !Prefs.profile then "-p" else ""
@@ -537,11 +534,6 @@ let camltag = match caml_version_list with
 
 (** * CamlpX configuration *)
 
-(** We assume that camlp(4|5) binaries are at the same place as ocaml ones
-    (this should become configurable some day). *)
-
-let camlp4bin = camlbin
-
 (* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
 (* TODO: remove the late attempts at finding gramlib.cma *)
 
@@ -564,7 +556,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
         camllib/"site-lib"/"camlp5"
       else ""
     in
-    (* if the two values are different than camlp5 has been relocated
+    (* if the two values are different then camlp5 has been relocated
      * and will not be able to find its own files, so we prefer the
      * path where the files actually do exist *)
     if dir2 = "" then
@@ -576,39 +568,39 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
     else dir2
 
 let check_camlp5_version () =
-  let s = camlexec.p4 in
-  (* translate 4 into 5 in the binary name *)
-  for i = 0 to String.length s - 1 do
-    if s.[i] = '4' then s.[i] <- '5'
-  done;
   try
-    let version_line, _ = run ~err:StdOut camlexec.p4 ["-v"] in
+    let camlp5o = which "camlp5o" in
+    let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
     let version = List.nth (string_split ' ' version_line) 2 in
     match string_split '.' version with
     | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
-      printf "You have Camlp5 %s. Good!\n" version
+      printf "You have Camlp5 %s. Good!\n" version; camlp5o
     | _ -> failwith "bad version"
-  with _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
+  with
+  | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
+  | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
 
 let config_camlpX () =
   try
     if not !Prefs.usecamlp5 then raise NoCamlp5;
-    let lib = "gramlib" in
-    let dir = check_camlp5 (lib^".cma") in
-    let () = check_camlp5_version () in
-    "camlp5", dir, lib
+    let camlp5mod = "gramlib" in
+    let camlp5libdir = check_camlp5 (camlp5mod^".cma") in
+    let camlp5o = check_camlp5_version () in
+    "camlp5", camlp5o, Filename.basename camlp5o, camlp5libdir, camlp5mod
   with NoCamlp5 ->
     (* We now try to use Camlp4, either by explicit choice or
        by lack of proper Camlp5 installation *)
-    let lib = "camlp4lib" in
-    let dir = camllib/"camlp4" in
-    if not (Sys.file_exists (dir/lib^".cma")) then
+    let camlp4mod = "camlp4lib" in
+    let camlp4libdir = camllib/"camlp4" in
+    if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then
       die "No Camlp4 installation found.\n";
-    let () = camlexec.p4 <- camlexec.p4 ^ "rf" in
-    ignore (run camlexec.p4 []);
-    "camlp4", dir, lib
+    try
+      let camlp4orf = which "camlp4orf" in
+      ignore (run camlp4orf []);
+      "camlp4", camlp4orf, Filename.basename camlp4orf, camlp4libdir, camlp4mod
+    with _ -> die "No Camlp4 installation found.\n"
 
-let camlp4, fullcamlp4lib, camlp4mod = config_camlpX ()
+let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod = config_camlpX ()
 
 let shorten_camllib s =
   if starts_with s (camllib^"/") then
@@ -616,8 +608,7 @@ let shorten_camllib s =
     "+" ^ String.sub s l (String.length s - l)
   else s
 
-let camlp4lib = shorten_camllib fullcamlp4lib
-
+let camlpXlibdir = shorten_camllib fullcamlpXlibdir
 
 (** * Native compiler *)
 
@@ -627,8 +618,8 @@ let msg_byteonly () =
 let msg_no_ocamlopt () =
   printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly ()
 
-let msg_no_camlp4_cmxa () =
-  printf "Cannot find the native-code library of %s.\n" camlp4; msg_byteonly ()
+let msg_no_camlpX_cmxa () =
+  printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly ()
 
 let msg_no_dynlink_cmxa () =
   printf "Cannot find native-code dynlink library.\n"; msg_byteonly ();
@@ -643,8 +634,8 @@ let check_native () =
     reset_caml_opt camlexec camloptopt
   else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then
     (msg_no_ocamlopt (); raise Not_found);
-  if not (Sys.file_exists (fullcamlp4lib/camlp4mod^".cmxa")) then
-    (msg_no_camlp4_cmxa (); raise Not_found);
+  if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) then
+    (msg_no_camlpX_cmxa (); raise Not_found);
   if not (Sys.file_exists (camllib/"dynlink.cmxa")) then
     (msg_no_dynlink_cmxa (); raise Not_found);
   let version, _ = run camlexec.opt ["-version"] in
@@ -969,7 +960,7 @@ let print_summary () =
   pr "  OCaml/Camlp4 version        : %s\n" caml_version;
   pr "  OCaml/Camlp4 binaries in    : %s\n" camlbin;
   pr "  OCaml library in            : %s\n" camllib;
-  pr "  Camlp4 library in           : %s\n" camlp4lib;
+  pr "  %s library in           : %s\n"     (String.capitalize camlpX) camlpXlibdir;
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
@@ -1009,7 +1000,7 @@ let write_dbg_wrapper f =
   pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n";
   pr "export COQTOP=%S\n" coqtop;
   pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug");
-  pr "CAMLP4LIB=%S\n\n" camlp4lib;
+  pr "CAMLP4LIB=%S\n\n" camlpXlibdir;
   pr ". $COQTOP/dev/ocamldebug-coq.run\n";
   close_out o;
   Unix.chmod f 0o555
@@ -1048,10 +1039,10 @@ let write_configml f =
   pr_s "ocamllex" camlexec.lex;
   pr_s "camlbin" camlbin;
   pr_s "camllib" camllib;
-  pr_s "camlp4" camlp4;
-  pr_s "camlp4o" camlexec.p4;
-  pr_s "camlp4bin" camlp4bin;
-  pr_s "camlp4lib" camlp4lib;
+  pr_s "camlp4" camlpX;
+  pr_s "camlp4o" camlpXo;
+  pr_s "camlp4bin" camlpXbindir;
+  pr_s "camlp4lib" camlpXlibdir;
   pr_s "camlp4compat" camlp4compat;
   pr_s "cflags" cflags;
   pr_s "best" best_compiler;
@@ -1159,10 +1150,10 @@ let write_makefile f =
   pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag;
   pr "# Camlp4 : flavor, binaries, libraries ...\n";
   pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
-  pr "CAMLP4=%s\n" camlp4;
-  pr "CAMLP4O=%S\n" camlexec.p4;
+  pr "CAMLP4=%s\n" camlpX;
+  pr "CAMLP4O=%S\n" camlpXo;
   pr "CAMLP4COMPAT=%s\n" camlp4compat;
-  pr "MYCAMLP4LIB=%S\n\n" camlp4lib;
+  pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir;
   pr "# Your architecture\n";
   pr "# Can be obtain by UNIX command arch\n";
   pr "ARCH=%s\n" arch;
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 96b486cdfa..069b991274 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -326,7 +326,8 @@ An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$}
 can be put after the name of the instance and before the colon to
 declare a parameterized instance.
 An optional \textit{priority} can be declared, 0 being the highest
-priority as for auto hints.
+priority as for auto hints. If the priority is not specified, it defaults to
+$n$, the number of binders of the instance.
 
 \begin{Variants}
 \item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index eea53886b8..186bc9add3 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -142,7 +142,7 @@ is understood as
 & | & {\tt idtac} \sequence{\messagetoken}{}\\
 & | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
 & | & {\tt gfail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
-& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
+& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}|~ {\tt fresh} {\qualid}\\
 & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
 & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
 & | & {\tt type of} {\term}\\
@@ -906,8 +906,8 @@ The following expression returns an identifier:
 \end{quote}
 It evaluates to an identifier unbound in the goal. This fresh
 identifier is obtained by concatenating the value of the
-\textrm{\textsl{component}}'s (each of them is, either an {\ident} which
-has to refer to a name, or directly a name denoted by a
+\textrm{\textsl{component}}'s (each of them is, either an {\qualid} which
+has to refer to a (unqualified) name, or directly a name denoted by a
 {\qstring}). If the resulting name is already used, it is padded
 with a number so that it becomes fresh. If no component is
 given, the name is a fresh derivative of the name {\tt H}.
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8ba1c8ecd2..1800cb8fe8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -662,10 +662,14 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      buffer#remove_tag Tags.Script.read_only ~start ~stop;
+      buffer#remove_tag Tags.Script.error ~start ~stop;
+      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
-    List.iter (fun { stop } -> buffer#delete_mark stop) seg
+    List.iter (fun { stop } -> buffer#delete_mark stop) seg;
+    self#print_stack
 
   (** Wrapper around the raw undo command *)
   method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49f748412a..e823c01b17 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -464,55 +464,22 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and
+   [c2] (using [k1] to expose the structure of [c1] and [k2] to expose
+   the structure [c2]) using [eq] to compare the immediate subterms of
+   [c1] of [c2] for conversion if needed, [leq] for cumulativity, [u]
+   to compare universe instances, and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account. Note that as [kind1] and [kind2] are
+   potentially different, we cannot use, in recursive case, the
+   optimisation that physically equal arrays are equals (hence the
+   calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen eq_universes eq_sorts f t1 t2 =
-  match kind t1, kind t2 with
+let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+  match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
-  | Sort s1, Sort s2 -> eq_sorts s1 s2
-  | Cast (c1,_,_), _ -> f c1 t2
-  | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
-  | App (Cast(c1, _, _),l1), _ -> f (mkApp (c1,l1)) t2
-  | _, App (Cast (c2, _, _),l2) -> f t1 (mkApp (c2,l2))
-  | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      f c1 c2 && Array.equal f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
-  | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
-  | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
-  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
-  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | _ -> false
-
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
-
-(* [compare_head_gen_leq u s sl eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
-   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
-   [u] to compare universe instances and [s] to compare sorts; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
-  match kind t1, kind t2 with
-  | Rel n1, Rel n2 -> Int.equal n1 n2
-  | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
   | Sort s1, Sort s2 -> leq_sorts s1 s2
   | Cast (c1,_,_), _ -> leq c1 t2
   | _, Cast (c2,_,_) -> leq t1 c2
@@ -522,8 +489,8 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      eq c1 c2 && Array.equal eq l1 l2
+      Int.equal (Array.length l1) (Array.length l2) &&
+        eq c1 c2 && Array.equal_norefl eq l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
@@ -533,11 +500,31 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
       eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
       Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | _ -> false
 
+(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
+   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
+   [u] to compare universe instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
+  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
+   instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
+
+let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
+
 (*******************************)
 (*  alpha conversion functions *)
 (*******************************)
@@ -549,6 +536,14 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
+let rec equal_with kind1 kind2 m n =
+  (* note that pointer equality is not sufficient to ensure equality
+     up to [eq_evars], because we may evaluates evars of [m] and [n]
+     in different evar contexts. *)
+  let req_constr m n = equal_with kind1 kind2 m n in
+  compare_head_gen_with kind1 kind2
+    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
+
 let eq_constr_univs univs m n =
   if m == n then true
   else 
@@ -570,7 +565,7 @@ let leq_constr_univs univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
       compare_leq m n
 
@@ -620,7 +615,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 5d11511b4d..67d1adedf6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,6 +203,14 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
+(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
+    alpha, casts, application grouping, and using [k1] to expose the
+    head of [a] and [k2] to expose the head of [b]. *)
+val equal_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  constr -> constr -> bool
+
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
@@ -285,16 +293,15 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
-(** [compare_head_gen_leq u s sle f fle c1 c2] compare [c1] and [c2]
-    using [f] to compare the immediate subterms of [c1] of [c2] for
+(** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
+    [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
     instances (the first boolean tells if they belong to a constant),
-    [s] to compare sorts for equality and [sle] for subtyping; Cast's,
-    binders name and Cases annotations are not taken into account *)
+    [s] to compare sorts for for subtyping; Cast's, binders name and
+    Cases annotations are not taken into account *)
 
 val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (Sorts.t -> Sorts.t -> bool) ->
   (constr -> constr -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 1603454304..bb1e335468 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -13,6 +13,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   val is_empty : 'a array -> bool
   val exists : ('a -> bool) -> 'a array -> bool
   val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -85,19 +86,22 @@ let compare cmp v1 v2 =
       in
       loop (len - 1)
 
+let equal_norefl cmp t1 t2 =
+  let len = Array.length t1 in
+  if not (Int.equal len (Array.length t2)) then false
+  else
+    let rec aux i =
+      if i < 0 then true
+      else
+        let x = uget t1 i in
+        let y = uget t2 i in
+        cmp x y && aux (pred i)
+    in
+    aux (len - 1)
+
 let equal cmp t1 t2 =
-  if t1 == t2 then true else
-    let len = Array.length t1 in
-    if not (Int.equal len (Array.length t2)) then false
-    else
-      let rec aux i =
-        if i < 0 then true
-        else
-          let x = uget t1 i in
-          let y = uget t2 i in
-          cmp x y && aux (pred i)
-      in
-      aux (len - 1)
+  if t1 == t2 then true else equal_norefl cmp t1 t2
+    
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 39c35e2d54..7e5c93b5da 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -17,6 +17,11 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   (** Lift equality to array type. *)
 
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Like {!equal} but does not assume that equality is reflexive: no
+      optimisation is performed if both arrays are physically the
+      same. *)
+
   val is_empty : 'a array -> bool
   (** True whenever the array is empty. *)
 
diff --git a/lib/cString.ml b/lib/cString.ml
index 250b7cee2d..e9006860fd 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -135,7 +135,14 @@ let plural n s = if n<>1 then s^"s" else s
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
 
 let ordinal n =
-  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
   string_of_int n ^ s
 
 (* string parsing *)
diff --git a/lib/pp.ml b/lib/pp.ml
index cc56e5e8d7..76046a7f91 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -517,8 +517,17 @@ let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
+(** TODO: merge with CString.ordinal *)
 let pr_nth n =
-  int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th")
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
+  int n ++ str s
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
diff --git a/library/states.ml b/library/states.ml
index a1c2a095d0..96a487b160 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,6 +12,7 @@ open System
 type state = Lib.frozen * Summary.frozen
 
 let summary_of_state = snd
+let replace_summary (lib,_) s = lib, s
 
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
diff --git a/library/states.mli b/library/states.mli
index 66de14909a..4d5d63e037 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
 val summary_of_state : state -> Summary.frozen
+val replace_summary : state -> Summary.frozen -> state
 
 (** {6 Rollback } *)
 
diff --git a/library/universes.ml b/library/universes.ml
index 79070763ec..51c2b4d851 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -165,7 +165,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts 
+      Constr.compare_head_gen_leq eq_universes leq_sorts 
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
@@ -213,7 +213,7 @@ let leq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b4d96e5cb1..3cd7dbc9be 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -153,8 +153,12 @@ GEXTEND Gram
       | IDENT "type_term"; c=uconstr -> TacPretype c
       | IDENT "numgoals" -> TacNumgoals ] ]
   ;
+  (* If a qualid is given, use its short name. TODO: have the shortest
+     non ambiguous name where dots are replaced by "_"? Probably too
+     verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ]
+    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
+	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7110e5b232..8884aef1cf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,7 +23,7 @@ open Pp
 open Errors
 open Util
 
-let reference dir s = Coqlib.gen_reference "CC" dir s
+let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
 let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -91,7 +91,7 @@ let atom_of_constr env sigma term =
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -126,7 +126,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -147,7 +147,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -159,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -246,10 +246,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k = 
-  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k = 
-  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
@@ -375,9 +375,9 @@ let discriminate_tac (cstr,u as cstru) p =
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
-    let identity = Universes.constr_of_global _I in
+    let identity = Universes.constr_of_global (Lazy.force _I) in
     (* let trivial=pf_type_of gls identity in *)
-    let trivial = Universes.constr_of_global _True in
+    let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
@@ -493,7 +493,7 @@ let f_equal =
     in
     Proofview.tclORELSE
       begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
+      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
 	  begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b01f29a40a..f355d9a725 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -121,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
-  | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+  | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+  | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+  | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
@@ -178,7 +178,9 @@ let restrict_instance evd evk filter argsv =
   Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
 let noccur_evar env evd evk c =
-  let rec occur_rec k c = match kind_of_term c with
+  let cache = ref Int.Set.empty (* cache for let-ins *) in
+  let rec occur_rec k c =
+  match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
        | Some c -> occur_rec k c
@@ -186,9 +188,10 @@ let noccur_evar env evd evk c =
            if Evar.equal evk evk' then raise Occur
            else Array.iter (occur_rec k) args')
   | Rel i when i > k ->
+      if not (Int.Set.mem (i-k) !cache) then
       (match pi2 (Environ.lookup_rel (i-k) env) with
        | None -> ()
-       | Some b -> occur_rec k (lift i b))
+       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b))
   | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
   | _ -> iter_constr_with_binders succ occur_rec k c
   in
@@ -315,6 +318,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+  let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
     | Rel n -> Int.Set.mem (n-depth) !cache_rel
@@ -329,8 +333,13 @@ let free_vars_and_rels_up_alias_expansion aliases c =
     | Rel _ | Var _ as ck ->
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c = expansion_of_var aliases c in
+      let c' = expansion_of_var aliases c in
+      (if c != c' then (* expansion, hence a let-in *)
         match kind_of_term c with
+        | Var id -> acc4 := Id.Set.add id !acc4
+        | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
+        | _ -> ());
+      match kind_of_term c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
@@ -342,7 +351,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
           frec (aliases,depth) c
   in
   frec (aliases,0) c;
-  (!acc1,!acc2)
+  (!acc1,!acc2,!acc3,!acc4)
 
 (********************************)
 (* Managing pattern-unification *)
@@ -378,7 +387,7 @@ let get_actual_deps aliases l t =
     l
   else
     (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
     List.filter (fun c ->
       match kind_of_term c with
       | Var id -> Id.Set.mem id fv_ids
@@ -1017,29 +1026,42 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args = decompose_app_vect t in
+let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+  let f,args2 = decompose_app_vect t in
+  let f,args1 = decompose_app_vect (whd_evar evd f) in
+  let args = Array.append args1 args2 in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false force k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false force k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2
-  | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+  | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
+  | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
 
-let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t =
-  let t = expansion_of_var aliases t in
-  match kind_of_term t with
-  | Var id -> Id.Set.mem id fv_ids
-  | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true force k (ev,fvs) t
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
+  let t' = expansion_of_var aliases t in
+  if t' != t then
+    (* t is a local definition, we keep it only if appears in the list *)
+    (* of let-in variables effectively occurring on the right-hand side, *)
+    (* which is the only reason to keep it when inverting arguments *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id let_ids
+    | Rel n -> Int.Set.mem n let_rels
+    | _ -> assert false
+  else
+    (* t is an instance for a proper variable; we filter it along *)
+    (* the free variables allowed to occur *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id fv_ids
+    | Rel n -> n <= k || Int.Set.mem n fv_rels
+    | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
@@ -1049,7 +1071,7 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases force k2 evk2 fvs2)
+    (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
@@ -1111,13 +1133,13 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
     with CannotProject (evd,ev2) ->
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d286b98e83..201a16ebeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
@@ -838,3 +842,8 @@ let subterm_source evk (loc,k) =
     | Evar_kinds.SubEvar (evk) -> evk
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to isntantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (Reductionops.whd_evar sigma t)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f89266a60a..49036798e6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 exception Uninstantiated_evar of existential_key
 val flush_and_check_evars :  evar_map -> constr -> constr
 
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+    value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
@@ -236,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9313e22320..454c51195b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -568,14 +568,6 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-(* HH: The progress tactical now uses this function. *)
-let progress_evar_map d1 d2 =
-  let is_new k v =
-    assert (v.evar_body == Evar_empty);
-    EvMap.mem k d2.defn_evars
-  in
-  not (d1 == d2) && EvMap.exists is_new d1.undf_evars
-
 let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
   let id = match naming with
   | Misctypes.IntroAnonymous ->
@@ -779,7 +771,9 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+  else {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
@@ -1301,27 +1295,6 @@ let e_eq_constr_univs evdref t u =
 let eq_constr_univs_test evd t u =
   snd (eq_constr_univs evd t u)
 
-let eq_named_context_val d ctx1 ctx2 = 
-  ctx1 == ctx2 ||
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 
-      && (eq_constr_univs_test d) t1 t2
-    in List.equal eq_named_declaration c1 c2
-
-let eq_evar_body d b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
-| _ -> false
-
-let eq_evar_info d ei1 ei2 =
-  ei1 == ei2 ||
-    eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
-    eq_evar_body d ei1.evar_body ei2.evar_body
-    (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cf6ba07c60..0765b951fd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -126,10 +126,6 @@ type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
 
-val progress_evar_map : evar_map -> evar_map -> bool
-(** Assuming that the second map extends the first one, this says if
-   some existing evar has been refined *)
-
 val empty : evar_map
 (** The empty evar map. *)
 
@@ -204,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
 val undefined_map : evar_map -> evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
-(** Compare the evar_info's up to the universe constraints of the evar map. *)
-
 val drop_all_defined : evar_map -> evar_map
 
 (** {6 Instantiating partial terms} *)
@@ -397,7 +390,7 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b6861fd499..6f62634133 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -719,22 +719,72 @@ let give_up =
 
 (** {7 Control primitives} *)
 
-(** Equality function on goals *)
-let goal_equal evars1 gl1 evars2 gl2 =
-  let evi1 = Evd.find evars1 gl1 in
-  let evi2 = Evd.find evars2 gl2 in
-  Evd.eq_evar_info evars2 evi1 evi2
+
+module Progress = struct
+
+  (** equality function up to evar instantiation in heterogeneous
+      contexts. *)
+  (* spiwack (2015-02-19): In the previous version of progress an
+     equality which considers two universes equal when it is consistent
+     tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
+     behaviour has to be restored as well. This has to be established by
+     practice. *)
+    
+  let rec eq_constr sigma1 sigma2 t1 t2 =
+    Constr.equal_with
+      (fun t -> Evarutil.kind_of_term_upto sigma1 t)
+      (fun t -> Evarutil.kind_of_term_upto sigma2 t)
+      t1 t2
+
+  (** equality function on hypothesis contexts *)
+  let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
+    let open Environ in
+    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
+      && (eq_constr sigma1 sigma2) t1 t2
+    in List.equal eq_named_declaration c1 c2
+
+  let eq_evar_body sigma1 sigma2 b1 b2 =
+    let open Evd in
+    match b1, b2 with
+    | Evar_empty, Evar_empty -> true
+    | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
+    | _ -> false
+
+  let eq_evar_info sigma1 sigma2 ei1 ei2 =
+    let open Evd in
+    eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
+    eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
+    eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
+
+  (** Equality function on goals *)
+  let goal_equal evars1 gl1 evars2 gl2 =
+    let evi1 = Evd.find evars1 gl1 in
+    let evi2 = Evd.find evars2 gl2 in
+    eq_evar_info evars1 evars2 evi1 evi2
+
+end
 
 let tclPROGRESS t =
   let open Proof in
   Pv.get >>= fun initial ->
   t >>= fun res ->
   Pv.get >>= fun final ->
+  (* [*_test] test absence of progress. [quick_test] is approximate
+     whereas [exhaustive_test] is complete. *)
+  let quick_test =
+    initial.solution == final.solution && initial.comb == final.comb
+  in
+  let exhaustive_test =
+    Util.List.for_all2eq begin fun i f ->
+      Progress.goal_equal initial.solution i final.solution f
+    end initial.comb final.comb
+  in
   let test =
-    Evd.progress_evar_map initial.solution final.solution &&
-    not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb)
+    quick_test || exhaustive_test
   in
-  if test then
+  if not test then
     tclUNIT res
   else
     tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
diff --git a/stm/stm.ml b/stm/stm.ml
index a4db934b25..5edf480446 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -161,6 +161,11 @@ type step =
   | `Alias  of alias_t ]
 type visit = { step : step; next : Stateid.t }
 
+
+(* Parts of the system state that are morally part of the proof state *)
+let summary_pstate = [ Evarutil.meta_counter_summary_name;
+                       Evarutil.evar_counter_summary_name;
+                       "program-tcc-table" ]
 type state = {
   system : States.state;
   proof : Proof_global.state;
@@ -594,9 +599,12 @@ module State : sig
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
   val same_env : frozen_state -> frozen_state -> bool
+
+  type proof_part
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  val proof_part_of_frozen : frozen_state -> Proof_global.state
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
 end = struct (* {{{ *)
@@ -620,9 +628,14 @@ end = struct (* {{{ *)
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
+  type proof_part =
+    Proof_global.state * Summary.frozen_bits (* only meta counters *)
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  let proof_part_of_frozen { proof } = proof
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  let proof_part_of_frozen { proof; system } =
+    proof,
+    Summary.project_summary (States.summary_of_state system) summary_pstate
 
   let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
 
@@ -657,9 +670,16 @@ end = struct (* {{{ *)
     if VCS.get_state id <> None then () else
     try match what with
     | `Full s -> VCS.set_state id s
-    | `Proof(ontop,p) ->
-         if is_cached ontop then (
-           VCS.set_state id { (get_cached ontop) with proof = p })
+    | `Proof(ontop,(pstate,counters)) ->
+         if is_cached ontop then
+           let s = get_cached ontop in
+           let s = { s with proof = pstate } in
+           let s = { s with system =
+             States.replace_summary s.system
+               (Summary.surgery_summary
+                 (States.summary_of_state s.system)
+               counters) } in
+           VCS.set_state id s
     with VCS.Expired -> ()
 
   let exn_on id ?valid (e, info) =
@@ -1555,7 +1575,7 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+let pstate = summary_pstate
 
 let async_policy () =
   let open Flags in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index eaaef45fce..789bcd1bdd 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -133,6 +133,14 @@ let unify_e_resolve poly flags (c,clenv) gls =
     tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
       (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
 
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none db
+  | Some hdc ->
+    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
+    else (fun db -> Hint_db.map_auto hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
 let e_exact poly flags (c,clenv) =
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
@@ -155,16 +163,11 @@ let rec e_trivial_fail_db db_list local_db =
   end
 
 and e_my_find_search db_list local_db hdc concl =
+  let hint_of_db = hintmap_of hdc concl in
   let hintl =
-    if occur_existential concl then
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
-   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
-    else
-      List.map_append (fun db ->
-	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -185,17 +188,14 @@ and e_my_find_search db_list local_db hdc concl =
   List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
-  try
-    priority
-      (e_my_find_search db_list local_db
-	 (decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try priority (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd
-    (e_my_find_search db_list local_db
-	(decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try List.map snd (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let find_first_goal gls =
   try first_goal gls with UserError _ -> assert false
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3b497faab5..af541b8b9e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-	   strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto.");
+	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
@@ -1973,6 +1973,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 trivial\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1984,6 +1990,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
   | TacAuto (debug,n,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_auto\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 auto\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 013270b0bd..ccf4795d68 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -882,7 +882,7 @@ let msg_quantified_hypothesis = function
   | NamedHyp id ->
       str "quantified hypothesis named " ++ pr_id id
   | AnonHyp n ->
-      int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+      pr_nth n ++
       str " non dependent hypothesis"
 
 let depth_of_quantified_hypothesis red h gl =
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/closed/3298.v
index bce7c3f23b..3a7de45670 100644
--- a/test-suite/bugs/opened/3298.v
+++ b/test-suite/bugs/closed/3298.v
@@ -4,8 +4,7 @@ Module JGross.
   Goal forall H : False, match H return Set with end.
   Proof.
     intros.
-    Fail solve [ eauto ]. (* No applicable tactic *)
-    admit.
+    solve [ eauto ].
   Qed.
 End JGross.
 
@@ -17,7 +16,6 @@ Section BenDelaware.
   Qed.
   Goal forall (H : False), match H return Set with end.
   Proof.
-    Fail solve [ eauto ] .
-    admit.
+    solve [ eauto ] .
   Qed.
 End BenDelaware.
diff --git a/test-suite/bugs/opened/3681.v b/test-suite/bugs/closed/3681.v
index 194113c6ed..194113c6ed 100644
--- a/test-suite/bugs/opened/3681.v
+++ b/test-suite/bugs/closed/3681.v
diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
deleted file mode 100644
index 24f340bbd9..0000000000
--- a/test-suite/bugs/closed/4035.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Use of dependent destruction from ltac *)
-Require Import Program.
-Goal nat -> Type.
-  intro x.
-  lazymatch goal with
-  | [ x : nat |- _ ] => dependent destruction x
-  end.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
new file mode 100644
index 0000000000..0ccbf5652f
--- /dev/null
+++ b/test-suite/bugs/closed/4089.v
@@ -0,0 +1,373 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Open Scope type_scope.
+
+Global Set Universe Polymorphism.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+
+Ltac rapply p :=
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
+
+Local Unset Elimination Schemes.
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Ltac transitivity x := etransitivity x.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Definition paths_rect := paths_ind.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Local Open Scope path_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : f == g
+  := fun x => match h with idpath => 1 end.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Arguments eisadj {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Bind Scope equiv_scope with Equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ q
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+  := match r with idpath => 1 end.
+Module Export Equivalences.
+
+Generalizable Variables A B C f g.
+
+Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  BuildIsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+
+Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.
+
+Arguments equiv_idmap {A} , A.
+
+Notation "1" := equiv_idmap : equiv_scope.
+
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000
+  := BuildIsEquiv A C (compose g f)
+    (compose f^-1 g^-1)
+    (fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
+    (fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
+    (fun a =>
+      (whiskerL _ (eisadj g (f a))) @
+      (ap_pp g _ _)^ @
+      ap02 g
+      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
+        (ap_compose f^-1 f _ @@ eisadj f a) @
+        (ap_pp f _ _)^
+      ) @
+      (ap_compose f g _)^
+    ).
+
+Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
+  `{IsEquiv B C g} `{IsEquiv A B f}
+  : A <~> C
+  := BuildEquiv A C (compose g f) _.
+
+Global Instance transitive_equiv : Transitive Equiv | 0 :=
+  fun _ _ _ f g => equiv_compose g f.
+
+Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
+admit.
+Defined.
+
+Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.
+
+End Equivalences.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z').
+admit.
+Defined.
+
+Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
+: IsEquiv (path_prod_uncurried z z') | 0.
+admit.
+Defined.
+
+Definition equiv_path_prod {A B : Type} (z z' : A * B)
+  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
+  := BuildEquiv _ _ (path_prod_uncurried z z') _.
+
+Generalizable Variables X A B C f g n.
+
+Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) (g : forall a, P a -> Q (f a))
+: sigT P -> sigT Q
+  := fun u => (f u.1 ; g u.1 u.2).
+
+Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: IsEquiv (functor_sigma f g) | 1000.
+admit.
+Defined.
+
+Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) `{IsEquiv A B f}
+           (g : forall a, P a -> Q (f a))
+           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: sigT P <~> sigT Q
+  := BuildEquiv _ _ (functor_sigma f g) _.
+
+Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
+           (f : A <~> B)
+           (g : forall a, P a <~> Q (f a))
+: sigT P <~> sigT Q
+  := equiv_functor_sigma f g.
+
+Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
+           (g : forall a, P a <~> Q a)
+: sigT P <~> sigT Q
+  := equiv_functor_sigma' 1 g.
+
+Definition Bip : Type := { C : Type &  C * C }.
+
+Definition BipMor (X Y : Bip) : Type :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) =>
+    { f : C -> D & (f c0 = d0) * (f c1 = d1) }
+  end.
+
+Definition bipmor2map {X Y : Bip} : BipMor X Y -> X.1 -> Y.1 :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) => fun i =>
+    match i with (f;_) => f end
+  end.
+
+Definition bipidmor {X : Bip} : BipMor X X :=
+  match X with (C;(c0,c1)) => (idmap; (1, 1)) end.
+
+Definition bipcompmor {X Y Z : Bip} : BipMor X Y -> BipMor Y Z -> BipMor X Z :=
+  match X, Y, Z with (C;(c0,c1)), (D;(d0,d1)), (E;(e0,e1)) => fun i j =>
+    match i, j with (f;(f0,f1)), (g;(g0,g1)) =>
+      (g o f; (ap g f0 @ g0, ap g f1 @ g1))
+    end
+  end.
+
+Definition isbipequiv {X Y : Bip} (i : BipMor X Y) : Type :=
+  { l : BipMor Y X & bipcompmor i l = bipidmor } *
+  { r : BipMor Y X & bipcompmor r i = bipidmor }.
+
+Lemma bipequivEQequiv : forall {X Y : Bip} (i : BipMor X Y),
+  isbipequiv i <~> IsEquiv (bipmor2map i).
+Proof.
+assert (equivcompmor : forall {X Y : Bip} (i : BipMor X Y) j,
+(bipcompmor i j = bipidmor) <~> Unit).
+  intros; set (U := X); set (V := Y); destruct X as [C [c0 c1]], Y as [D [d0 d1]].
+  transitivity { n : (bipcompmor i j).1 = (@bipidmor U).1 &
+  (bipcompmor i j).2 = transport (fun h => (h c0 = c0) * (h c1 = c1)) n^ (@bipidmor U).2}.
+    admit.
+  destruct i as [f [f0 f1]]; destruct j as [g [g0 g1]].
+
+  transitivity { n : g o f = idmap & (ap g f0 @ g0 = apD10 n c0 @ 1) *
+  (ap g f1 @ g1 = apD10 n c1 @ 1)}.
+    apply equiv_functor_sigma_id; intro n.
+    assert (Ggen : forall (h0 h1 : C -> C) (p : h0 = h1) u0 u1 v0 v1,
+    ((u0, u1) = transport (fun h => (h c0 = c0) * (h c1 = c1)) p^ (v0, v1)) <~>
+    (u0 = apD10 p c0 @ v0) * (u1 = apD10 p c1 @ v1)).
+      induction p; intros; simpl; rewrite !concat_1p; apply symmetry.
+      by apply (equiv_path_prod (u0,u1) (v0,v1)).
+    rapply Ggen.
+    pose (@paths C).
+    Check (@paths C).
+    Undo.
+    Check (@paths C). (* Toplevel input, characters 0-17:
+Error: Illegal application:
+The term "@paths" of type "forall A : Type, A -> A -> Type"
+cannot be applied to the term
+ "C" : "Type"
+This term has type "Type@{Top.892}" which should be coercible to
+ "Type@{Top.882}".
+*)
diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
new file mode 100644
index 0000000000..3cf9e8b093
--- /dev/null
+++ b/test-suite/complexity/bug4076.v
@@ -0,0 +1,29 @@
+(* Check behavior of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i : nat), P i -> P i.
+Parameter P : nat -> Type.
+
+Time Definition g (n : nat) (a0 : P n) : P n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  a17.
diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
new file mode 100644
index 0000000000..f3996e6ae6
--- /dev/null
+++ b/test-suite/complexity/bug4076bis.v
@@ -0,0 +1,31 @@
+(* Another check of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i j : nat), P i j -> P i j.
+Parameter P : nat -> nat -> Type.
+
+Time Definition g (n : nat) (a0 : P n n) : P n n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  let a18 := f a17 in
+  let a19 := f a18 in
+  a19.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9e828e6ea0..a7d3f8062a 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -180,12 +180,14 @@ Ltac easy :=
     | H : _ |- _ => solve [inversion H]
     | _ => idtac
     end in
-  let rec do_atom :=
-    solve [reflexivity | symmetry; trivial] ||
-    contradiction ||
-    (split; do_atom)
-  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
-  (use_hyps; do_ccl) || fail "Cannot solve this goal".
+  let do_atom :=
+    solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ] in
+  let rec do_ccl :=
+    try do_atom;
+    repeat (do_intro; try do_atom);
+    solve [ split; do_ccl ] in
+  solve [ do_atom | use_hyps; do_ccl ] ||
+  fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 4b02873172..ae6fe7dd0a 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -433,40 +433,40 @@ Ltac do_depelim' rev tac H :=
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Tactic Notation "dependent" "destruction" hyp(H) := 
+Tactic Notation "dependent" "destruction" ident(H) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the elimination. *)
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
-Tactic Notation "dependent" "induction" hyp(H) :=
+Tactic Notation "dependent" "induction" ident(H) :=
   do_depind ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "using" constr(c) :=
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
   do_depind ltac:(fun hyp => induction hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) :=
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5213d38e71..84b4b5e5df 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,8 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
   [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
-  ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value]
+  ... [-I dir] ... [-R physicalpath logicalpath]
+  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
   ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
   [-h] [--help]
 
@@ -157,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
   |l ->
     try
       let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
-      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in
       (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
     with Not_found ->
       (
@@ -297,7 +298,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && ";
       printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
     in
-    print "uninstall_me.sh:\n";
+    printf "uninstall_me.sh: %s\n" !makefile_name;
     print "\techo '#!/bin/sh' > $@ \n";
     if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
     uninstall_by_root where_what_oth;
@@ -701,9 +702,12 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
   main_targets vfiles mlfiles other_targets inc;
     print ".PHONY: ";
     print_list " "
-      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" ::
-	  "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" ::
-	  "html" :: "validate" ::
+      ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" ::
+	  "gallina" :: "gallinahtml" :: "html" ::
+	  "install" :: "install-doc" :: "install-natdynlink" :: "install-toploop" ::
+	  "opt" :: "printenv" :: "quick" ::
+	  "uninstall" :: "userinstall" ::
+	  "validate" :: "vio2vo" ::
 	    (sds@(CList.map_filter
 		    (fun (n,_,is_phony,_) ->
 		     if is_phony then Some n else None) sps)));
@@ -764,10 +768,10 @@ let check_overlapping_include (_,inc_i,inc_r) =
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
+	  Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
 	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
-	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
+	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
   in aux (inc_i@inc_r)
 
 let do_makefile args =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 743cfaccdb..a2d2e3d91c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1501,7 +1501,7 @@ let vernac_check_may_eval redexp glopt rc =
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
   let uctx = Evd.universe_context sigma' in
-  let env = Environ.push_context uctx env in
+  let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
     if Evarutil.has_undefined_evars sigma' c then