Merge branch 'v8.5'

42 files changed, 329 insertions, 163 deletions

diff --git a/CHANGES b/CHANGES
index ca31ca2398..8b4a4fc933 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,6 +22,10 @@ Logic
   the return predicate. Restores compatibility of Coq's logic with the
   propositional extensionality axiom. May create incompatibilities in
   recursive programs heavily using dependent types.
+- Trivial inductive types are no longer defined in Type but in Prop, which
+  leads to a non-dependent induction principle being generated in place of
+  the dependent one. To recover the old behavior, explicitly define your
+  inductive types in Set.
 
 Vernacular commands
 
@@ -59,6 +63,8 @@ Vernacular commands
   retrieved using the "Locate Term" command.
 - New "Derive" command to help writing program by derivation.
 - "Undo" undoes any command, not just tactics.
+- "Undo. Undo." does not work in CoqIDE or Proof General, it works only
+  in coqtop.  "Undo 2" should be used intead.
 - New "Refine Instance Mode" option that allows to deactivate the generation of
   obligations in incomplete typeclass instances, raising an error instead.
 - "Collection" command to name sets of section hypotheses.  Named collections
@@ -70,6 +76,9 @@ Vernacular commands
   the execution of the following tactics.
 - "Optimize Heap" command to tell the OCaml runtime to perform a major
   garbage collection step and heap compaction.
+- "Instance" no longer treats the {|...|} syntax specially; it handles it
+  in the same way as other commands, e.g. "Definition". Use the {...}
+  syntax (no pipe symbols) to recover the old behavior.
 
 Specification Language
 
diff --git a/COMPATIBILITY b/COMPATIBILITY
index eeb0c292b1..2b3862eb08 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -62,6 +62,13 @@ Type classes.
   type information and switching to proof mode is no longer available.
   Use { } (without the vertical bars) instead.
 
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+  the global environment and inlined in the proof term when a proof
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
+  proofs with "Qed export" or "Qed export ident, .., ident".
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
diff --git a/Makefile.build b/Makefile.build
index 0d87d98e96..c3936c1a7a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -388,7 +388,7 @@ install-ide-info:
 $(COQIDEAPP)/Contents:
 	rm -rdf $@
 	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
 	$(MKDIR) "$@/MacOS"
 
 $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
diff --git a/Makefile.common b/Makefile.common
index d752a5be91..e548619610 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -207,12 +207,21 @@ ifneq ($(HASNATDYNLINK),false)
  PLUGINS:=$(PLUGINSCMA)
  PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
 else
+ifeq ($(BEST),byte)
+ STATICPLUGINS:=
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
+	$(FUNINDCMA) $(NATSYNTAXCMA)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+else
  STATICPLUGINS:=$(PLUGINSCMA)
  INITPLUGINS:=
  INITPLUGINSOPT:=
  PLUGINS:=
  PLUGINSOPT:=
 endif
+endif
 
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
diff --git a/README.win b/README.win
index 5027016f54..8302a707f6 100644
--- a/README.win
+++ b/README.win
@@ -8,10 +8,10 @@ INSTALLATION.
 
     The Coq package for Windows comes with an auto-installer. It will
 install Coq binaries and libraries under any directory you specify
-(C:\Program Files\Coq is the default path). It also creates shortcuts
-in the Windows menus. Alternatively, you can launch Coq using coqide.exe
-or coqtop.exe in the bin sub-directory of the installation
-(C:\Program Files\Coq\bin by default).
+(C:\Coq is the default path). It also creates shortcuts
+in the Windows menus.  Binaries, like coqc.exe,
+are in the bin sub-directory of the installation
+(C:\Coq\bin by default).
 
 COMPILATION.
 ============
@@ -20,40 +20,25 @@ COMPILATION.
     distribution. If you really need to recompile under Windows, here
     are some indications:
 
-    1- Install ocaml for Windows (MinGW port).
-       See: http://caml.inria.fr
+    1- Install cygwin and the wget package
+       See: http://cygwin.com
 
-    2- Install a shell environment with at least:
-         - a C compiler (gcc),
-         - the GNU make utility
+    2- Download and unzip in C:\ the SDK for windows
+       See: https://coq.inria.fr/distrib/current/files/
 
-       The Cygwin environment is well suited for compiling Coq
-       (official packages are made using Cygwin) See:
-       http://www.cygwin.com
+    3- From the cygwin prompt type
 
-    3- In order to compile Coqide, you will need the LablGTK library
-       See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
+        . /cygdrive/c/CoqSDK-85-1/environ
 
-       You also need to install the GTK libraries for Windows (see the
-       installation instruction for LablGTK)
+       The first time the script installs the C toolchain.
 
-    4- In a shell window, type successively
+    4- Then Coq can be compiled as follows:
+ 
+        ./configure -local
+        make
 
-        ./configure
-        make world
-        make install
+    5- To build the installer, type:
 
-    5- Though not nescessary, you can find useful:
-         - Windows version of (X)Emacs: it is a powerful environment for
-           developpers with coloured syntax, modes for compilation and debug,
-           and many more. It is free. See: http://www.gnu.org/software.
-         - Windows subversion client (very useful if you have access to the Coq
-           archive).
-
-    Good luck :-)
-
-    Alternatively, it is now possible (and even recommended ...) to build
-    Windows executables of coq from Linux thanks to a mingw cross-compiler.
-    If interested, please contact us for more details.
+        dev/make-installer-win32.sh
 
     The Coq Team.
diff --git a/configure.ml b/configure.ml
index 3aeb324c3b..fbfd8833b9 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1124,7 +1124,8 @@ let write_makefile f =
   List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
   List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
   pr "\n# Coq version\n";
-  pr "VERSION=%s\n\n" coq_version;
+  pr "VERSION=%s\n" coq_version;
+  pr "VERSION4MACOS=%s\n\n" coq_macos_version;
   pr "# Objective-Caml compile command\n";
   pr "OCAML=%S\n" camlexec.top;
   pr "OCAMLC=%S\n" camlexec.byte;
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 689ac14254..1704b4d60b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1010,13 +1010,19 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export}
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
+Such auxiliary lemma is inlined in the final proof term
+unless the proof is ended with ``\texttt{Qed export}''.  In such
+case the lemma is preserved.  The syntax
+``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$''
+is also supported.  In such case the system checks that the names given by the
+user actually exist when the proof is ended.
 
 This tactical is useful with tactics such as \texttt{omega} or
 \texttt{discriminate} that generate huge proof terms. With that tool
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 668a68c9c7..9f4ddc8044 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -247,7 +247,7 @@ to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
 reflexivity. In cases where the equality is not between constructor
 forms though, one must help the automation by giving
-some arguments, using the {\tt specialize} tactic.
+some arguments, using the {\tt specialize} tactic for example.
 
 \begin{coq_example*}
 destruct D... apply weak ; apply ax. apply ax.
@@ -257,16 +257,24 @@ destruct D...
 Show.
 \end{coq_example}
 \begin{coq_example}
-  specialize (IHterm G empty).
+  specialize (IHterm G0 empty eq_refl).
 \end{coq_example}
 
-Then the automation can find the needed equality {\tt G = G} to narrow
-the induction hypothesis further. This concludes our example.
+Once the induction hypothesis has been narrowed to the right equality,
+it can be used directly. 
 
 \begin{coq_example}
-  simpl_depind.
+  apply weak, IHterm.
 \end{coq_example}
 
+If there is an easy first-order solution to these equations as in this subgoal, the
+{\tt specialize\_eqs} tactic can be used instead of giving explicit proof
+terms:
+
+\begin{coq_example}
+  specialize_eqs IHterm.
+\end{coq_example}
+This concludes our example.
 \SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
 
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template
index fd80c83969..e224e81204 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/MacOS/Info.plist.template
@@ -66,7 +66,7 @@
 	<key>CFBundleGetInfoString</key>
 	<string>Coq_vVERSION</string>
 	<key>NSHumanReadableCopyright</key>
-	<string>Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
+	<string>Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
 	<key>CFBundleHelpBookFolder</key>
 	<string>share/doc/coq/html/</string>
 	<key>CFAppleHelpAnchor</key>
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a869442696..84ef8f40db 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -243,7 +243,14 @@ let coqtop_path () =
 	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos
             in
 	    String.blit "coqtop" 0 prog i 6;
-	    if Sys.file_exists prog then prog else "coqtop"
+	    if Sys.file_exists prog then prog
+	    else
+	      let in_macos_bundle =
+		Filename.concat
+		  (Filename.dirname prog)
+		  (Filename.concat "../Resources/bin" (Filename.basename prog))
+	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
+		 else "coqtop"
 	  with Not_found -> "coqtop"
   in file
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 25712f951b..9a4fde2f6e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -144,6 +144,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
@@ -220,10 +221,11 @@ let current = {
     vertical_tabs = false;
     opposite_tabs = false;
 
-    background_color = "cornsilk";
-    processed_color = "light green";
-    processing_color = "light blue";
-    error_color = "#FFCCCC";
+    background_color = Tags.default_color;
+    processed_color = Tags.default_processed_color;
+    processing_color = Tags.default_processing_color;
+    error_color = Tags.default_error_color;
+    error_fg_color = Tags.default_error_fg_color;
 
     dynamic_word_wrap = false;
     show_line_number = false;
@@ -296,6 +298,7 @@ let save_pref () =
     add "processing_color" [p.processing_color] ++
     add "processed_color" [p.processed_color] ++
     add "error_color" [p.error_color] ++
+    add "error_fg_color" [p.error_fg_color] ++
     add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++
     add "show_line_number" [string_of_bool p.show_line_number] ++
     add "auto_indent" [string_of_bool p.auto_indent] ++
@@ -382,6 +385,7 @@ let load_pref () =
     set_hd "processing_color" (fun v -> np.processing_color <- v);
     set_hd "processed_color" (fun v -> np.processed_color <- v);
     set_hd "error_color" (fun v -> np.error_color <- v);
+    set_hd "error_fg_color" (fun v -> np.error_fg_color <- v);
     set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v);
     set_bool "show_line_number" (fun v -> np.show_line_number <- v);
     set_bool "auto_indent" (fun v -> np.auto_indent <- v);
@@ -466,10 +470,15 @@ let configure ?(apply=(fun () -> ())) () =
       ~text:"Background color of errors"
       ~packing:(table#attach ~expand:`X ~left:0 ~top:3) ()
     in
+    let error_fg_label = GMisc.label
+      ~text:"Foreground color of errors"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:4) ()
+    in
     let () = background_label#set_xalign 0. in
     let () = processed_label#set_xalign 0. in
     let () = processing_label#set_xalign 0. in
     let () = error_label#set_xalign 0. in
+    let () = error_fg_label#set_xalign 0. in
     let background_button = GButton.color_button
       ~color:(Tags.color_of_string (current.background_color))
       ~packing:(table#attach ~left:1 ~top:0) ()
@@ -486,15 +495,19 @@ let configure ?(apply=(fun () -> ())) () =
       ~color:(Tags.get_error_color ())
       ~packing:(table#attach ~left:1 ~top:3) ()
     in
+    let error_fg_button = GButton.color_button
+      ~color:(Tags.get_error_fg_color ())
+      ~packing:(table#attach ~left:1 ~top:4) ()
+    in
     let reset_button = GButton.button
       ~label:"Reset"
       ~packing:box#pack ()
     in
     let reset_cb () =
-      background_button#set_color (Tags.color_of_string "cornsilk");
-      processing_button#set_color (Tags.color_of_string "light blue");
-      processed_button#set_color (Tags.color_of_string "light green");
-      error_button#set_color (Tags.color_of_string "#FFCCCC");
+      background_button#set_color Tags.(color_of_string default_color);
+      processing_button#set_color Tags.(color_of_string default_processing_color);
+      processed_button#set_color Tags.(color_of_string default_processed_color);
+      error_button#set_color Tags.(color_of_string default_error_color);
     in
     let _ = reset_button#connect#clicked ~callback:reset_cb in
     let label = "Color configuration" in
@@ -503,7 +516,12 @@ let configure ?(apply=(fun () -> ())) () =
       current.processing_color <- Tags.string_of_color processing_button#color;
       current.processed_color <- Tags.string_of_color processed_button#color;
       current.error_color <- Tags.string_of_color error_button#color;
-      !refresh_editor_hook ()
+      current.error_fg_color <- Tags.string_of_color error_fg_button#color;
+      !refresh_editor_hook ();
+      Tags.set_processing_color processing_button#color;
+      Tags.set_processed_color processed_button#color;
+      Tags.set_error_color error_button#color;
+      Tags.set_error_fg_color error_fg_button#color
     in
     custom ~label box callback true
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1b52d20a4c..ab12e4c7ba 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,6 +71,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
diff --git a/ide/tags.ml b/ide/tags.ml
index 04ad9a519c..079cf94853 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,15 +13,23 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
-let processed_color = ref "light green"
-let processing_color = ref "light blue"
-let error_color = ref "#FFCCCC"
+(* These work fine for colorblind people too *)
+let default_processed_color = "light green"
+let default_processing_color = "light blue"
+let default_error_color = "#FFCCCC"
+let default_error_fg_color = "red"
+let default_color = "cornsilk"
+
+let processed_color = ref default_processed_color
+let processing_color = ref default_processing_color
+let error_color = ref default_error_color
+let error_fg_color = ref default_error_fg_color
 
 module Script =
 struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
-  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"]
+  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
   let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
   let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
@@ -94,3 +102,11 @@ let set_error_color clr =
   let s = string_of_color clr in
   error_color := s;
   Script.error_bg#set_property (`BACKGROUND s)
+
+let get_error_fg_color () = color_of_string !error_fg_color
+
+let set_error_fg_color clr =
+  let s = string_of_color clr in
+  error_fg_color := s;
+  Script.error#set_property (`FOREGROUND s)
+
diff --git a/ide/tags.mli b/ide/tags.mli
index 9c3261d66d..e68015c991 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -53,3 +53,13 @@ val set_processing_color : Gdk.color -> unit
 
 val get_error_color : unit -> Gdk.color
 val set_error_color : Gdk.color -> unit
+
+val get_error_fg_color : unit -> Gdk.color
+val set_error_fg_color : Gdk.color -> unit
+
+val default_processed_color : string
+val default_processing_color : string
+val default_error_color : string
+val default_error_fg_color : string
+val default_color : string
+
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 3f2d002c77..07891d0b48 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -135,7 +135,7 @@ type search_restriction =
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
+type opacity_flag   = Opaque of lident list option | Transparent
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ea575e1e0d..799471c68a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -164,10 +164,12 @@ let infer_constructor_packet env_ar_par ctx params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,_,t as d) (lev,env) ->
-      let tj = infer_type env t in
-      let u = univ_of_sort tj.utj_type in
-	(Universe.sup u lev, push_rel d env))
+    (fun (_,b,t as d) (lev,env) ->
+      if Option.is_empty b then
+	let tj = infer_type env t in
+	let u = univ_of_sort tj.utj_type in
+	  (Universe.sup u lev, push_rel d env)
+      else lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
diff --git a/library/declare.ml b/library/declare.ml
index 7f42a747ed..c3181e4c75 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -253,24 +253,25 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
-  let cd = (* We deal with side effects of non-opaque constants *)
+let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let cd = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry ({
-      const_entry_opaque = false; const_entry_body = bo } as de)
-    | Entries.DefinitionEntry ({
-      const_entry_polymorphic = true; const_entry_body = bo } as de)
-      ->
-        let _, seff = Future.force bo in
-        if Declareops.side_effects_is_empty seff then cd
-        else begin
-          let seff = Declareops.uniquize_side_effects seff in
-          Declareops.iter_side_effects
-            (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-          Entries.DefinitionEntry { de with
-            const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-              pt, Declareops.no_seff) }
+    | Entries.DefinitionEntry de ->
+        if export_seff ||
+           not de.const_entry_opaque ||
+           de.const_entry_polymorphic then
+          let bo = de.const_entry_body in
+          let _, seff = Future.force bo in
+          if Declareops.side_effects_is_empty seff then cd
+          else begin
+            let seff = Declareops.uniquize_side_effects seff in
+            Declareops.iter_side_effects
+              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
+            Entries.DefinitionEntry { de with
+              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
+                pt, Declareops.no_seff) }
         end
+        else cd
     | _ -> cd
   in
   let cst = {
diff --git a/library/declare.mli b/library/declare.mli
index 03b66271a2..d8a00db0cf 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 27f14c7900..b23841ceff 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -52,15 +52,17 @@ GEXTEND Gram
       | IDENT "Existential"; n = natural; c = constr_body ->
 	  VernacSolveExistential (n,c)
       | IDENT "Admitted" -> VernacEndProof Admitted
-      | IDENT "Qed" -> VernacEndProof (Proved (true,None))
-      | IDENT "Save" -> VernacEndProof (Proved (true,None))
+      | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
+      | IDENT "Qed"; IDENT "export"; l = LIST0 identref SEP "," ->
+          VernacEndProof (Proved (Opaque (Some l),None))
+      | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
-	  VernacEndProof (Proved (true,Some (id,Some tok)))
+	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-	  VernacEndProof (Proved (true,Some (id,None)))
-      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+	  VernacEndProof (Proved (Opaque None,Some (id,None)))
+      | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
       |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (false,Some (id,None)))
+	  VernacEndProof (Proved (Transparent,Some (id,None)))
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 439b1a5c01..a77b552e01 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -55,7 +55,7 @@ let start_deriving f suchthat lemma =
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
-                opaque , f_def , lemma_def
+                opaque <> Vernacexpr.Transparent , f_def , lemma_def
             | _ -> assert false
       in
       (** The opacity of [f_def] is adjusted to be [false], as it
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index eb5221fd69..04347537f2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -989,7 +989,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.Proved(false,None))
+  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0c7b0a0b08..b9d7e0d909 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
+let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5558556e2d..b1cbea51c8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
   let ce = definition_entry ~univs:ctx value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
+let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -1247,9 +1247,9 @@ let build_new_goal_type () =
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
   match cb.Declarations.const_body with
-    | Declarations.OpaqueDef _ -> true
-    | Declarations.Undef _ -> true
-    | Declarations.Def _ -> false
+    | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
+    | Declarations.Undef _ -> Vernacexpr.Opaque None
+    | Declarations.Def _ -> Vernacexpr.Transparent
 
 let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 921609aae3..adfe9dd8de 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     in
       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
-    mkProd (na,u,refresh dir v)
+      mkProd (na,u,refresh dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
-  and refresh_term_evars onevars t =
+  and refresh_term_evars onevars top t =
     match kind_of_term t with
     | App (f, args) when is_template_polymorphic env f ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
+    | App (f, args) when top && isEvar f -> 
+      refresh_term_evars true false f; 
+      Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
       let ty' = refresh true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
-    | _ -> iter_constr (refresh_term_evars onevars) t
+    | _ -> iter_constr (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
     let rec aux i = function
       | Some l :: ls -> 
         if i < Array.length args then 
-	  ignore(refresh_term_evars true args.(i));
+	  ignore(refresh_term_evars true false args.(i));
         aux (succ i) ls
       | None :: ls -> 
         if i < Array.length args then 
-          ignore(refresh_term_evars false args.(i));
+          ignore(refresh_term_evars false false args.(i));
 	aux (succ i) ls
       | [] -> ()
     in aux 0 pos
@@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
       (match pbty with
       | None -> t
       | Some dir -> refresh dir t)
-    else (refresh_term_evars false t; t)
+    else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
 
@@ -1385,19 +1388,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
               imitate envk t in
 
-  let _fast rhs = 
-    let filter_ctxt = evar_filtered_context evi in
-    let names = ref Idset.empty in
-    let rec is_id_subst ctxt s =
-       match ctxt, s with
-         | ((id, _, _) :: ctxt'), (c :: s') ->
-           names := Idset.add id !names;
-           isVarId id c && is_id_subst ctxt' s'
-         | [], [] -> true
-         | _ -> false in
-    is_id_subst filter_ctxt (Array.to_list argsv) &&
-    closed0 rhs &&
-    Idset.subset (collect_vars rhs) !names in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a23963abca..6059e9ff84 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -842,7 +842,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		    let (tm',sk'),cst_l' =
 		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
 		    in
-		      if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk'
+		    let rec is_case x = match kind_of_term x with
+		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+		      | App (hd, _) -> is_case hd
+		      | Case _ -> true
+		      | _ -> false in
+		    if equal_stacks (x, app_sk) (tm', sk')
+		       || Stack.will_expose_iota sk'
+		       || is_case tm'
 		      then fold ()
 		      else whrec cst_l' (tm', sk' @ sk)
 		  else match recargs with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1106fefa39..372b26aa25 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -189,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
              if
 	       Array.for_all (noccurn k) tys
 	       && Array.for_all (noccurn (k+nbfix)) bds
+	       && k <= n
 	     then
 	       (k, List.nth labs (k-1))
 	     else
@@ -596,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c =
     | _ -> raise Redelimination
   in redrec c
 
-
-let dont_expose_case = function
-  | EvalVar _ | EvalRel _ | EvalEvar _ -> false
-  | EvalConst c ->
-     Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z)
-		 false (ReductionBehaviour.get (ConstRef c))
-
 let whd_nothing_for_iota env sigma s =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
@@ -1211,9 +1205,10 @@ let one_step_reduce env sigma c =
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_stack env) sigma fix stack with
+	  (try match reduce_fix (whd_construct_stack env) sigma fix stack with
              | Reduced s' -> s'
-	     | NotReducible -> raise NotStepReducible)
+	     | NotReducible -> raise NotStepReducible
+           with Redelimination -> raise NotStepReducible)
       | _ when isEvalRef env x ->
 	  let ref,u = destEvalRefU x in
           (try
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e9e335ec91..e0b94669c2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -740,9 +740,14 @@ module Make
 
         | VernacEndProof (Proved (opac,o)) -> return (
           match o with
-            | None -> if opac then keyword "Qed" else keyword "Defined"
+            | None -> (match opac with
+                | Transparent -> keyword "Defined"
+                | Opaque None -> keyword "Qed"
+                | Opaque (Some l) ->
+                    keyword "Qed" ++ spc() ++ str"export" ++
+                      prlist_with_sep (fun () -> str", ") pr_lident l)
             | Some (id,th) -> (match th with
-                | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+                | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
                 | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
         )
         | VernacExactProof c ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f2e6877989..63c45116a6 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -185,7 +185,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -200,7 +200,8 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
           | Local | Discharge -> true
           | Global -> false
           in
-          let kn = declare_constant id ~local (DefinitionEntry const, k) in
+          let kn =
+           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
     call_hook (fun exn -> exn) hook l r
@@ -273,25 +274,25 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
-let save_named proof =
+let save_named ?export_seff proof =
   let id,const,cstrs,do_guard,persistence,hook = proof in
-  save id const cstrs do_guard persistence hook
+  save ?export_seff id const cstrs do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 
-let save_anonymous proof save_ident =
+let save_anonymous ?export_seff proof save_ident =
   let id,const,cstrs,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs do_guard persistence hook
 
-let save_anonymous_with_strength proof kind save_ident =
+let save_anonymous_with_strength ?export_seff proof kind save_ident =
   let id,const,cstrs,do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
@@ -325,34 +326,50 @@ let get_proof proof do_guard hook opacity =
   (** FIXME *)
   id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
 
+let check_exist =
+  List.iter (fun (loc,id) ->
+    if not (Nametab.exists_cci (Lib.make_path id)) then
+        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
+  )
+
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit hook ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard hook is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit (hook None) ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard 
 	(hook (Some proof.Proof_global.universes)) is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
diff --git a/stm/stm.ml b/stm/stm.ml
index 693c673b40..207afd8aee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1035,7 +1035,7 @@ end = struct (* {{{ *)
         vernac_interp stop
           ~proof:(pobject, terminator)
           { verbose = false; loc;
-            expr = (VernacEndProof (Proved (true,None))) }) in
+            expr = (VernacEndProof (Proved (Opaque None,None))) }) in
       ignore(Future.join checked_proof);
       RespBuiltProof(proof,time)
     with
@@ -1166,7 +1166,7 @@ end = struct (* {{{ *)
       Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
         { verbose = false; loc;
-          expr = (VernacEndProof (Proved (true,None))) };
+          expr = (VernacEndProof (Proved (Opaque None,None))) };
       Some proof
     with e ->
       let (e, info) = Errors.push e in
@@ -1564,7 +1564,8 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined = function
-   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
+      true
    | _ -> false in
  let proof_using_ast = function
    | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0140f74f50..9289c6d663 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1464,28 +1464,32 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
           in Some proof
       in Some (Some (evars, res, newt))
 
+(** Insert a declaration after the last declaration it depends on *)
+let rec insert_dependent env decl accu hyps = match hyps with
+| [] -> List.rev_append accu [decl]
+| (id, _, _  as ndecl) :: rem ->
+  if occur_var_in_decl env id decl then
+    List.rev_append accu (decl :: hyps)
+  else
+    insert_dependent env decl (ndecl :: accu) rem
+
 let assert_replacing id newt tac = 
   let prf = Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let nc' =
-      Environ.fold_named_context
-        (fun _ (n, b, t as decl) nc' ->
-          if Id.equal n id then (n, b, newt) :: nc'
-          else decl :: nc')
-        env ~init:[]
+    let ctx = Environ.named_context env in
+    let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
+    let nc = match before with
+    | [] -> assert false
+    | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
     in
+    let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false begin fun sigma ->
-      let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
       let sigma, ev = Evarutil.new_evar env' sigma concl in
       let sigma, ev' = Evarutil.new_evar env sigma newt in
-      let fold _ (n, b, t) inst =
-        if Id.equal n id then ev' :: inst
-        else mkVar n :: inst
-      in
-      let inst = fold_named_context fold env ~init:[] in
-      let (e, args) = destEvar ev in
-      sigma, mkEvar (e, Array.of_list inst)
+      let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
+      let (e, _) = destEvar ev in
+      sigma, mkEvar (e, Array.map_of_list map nc)
     end
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 9e12b990b7..049589325e 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -315,8 +315,6 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setq
 intros; exact (@quotrel _ _).
 Defined.
 
-(* Unset Kernel Term Sharing. *)
-
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
 
 Definition ispartlbinopabmonoidfracrel_type : Type :=
@@ -326,3 +324,10 @@ Definition ispartlbinopabmonoidfracrel_type : Type :=
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
+Unset Kernel Term Sharing.
+
+Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
+
+Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+                                      ispartlbinopabmonoidfracrel_type in exact t)$.
+
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/closed/3490.v
index e7a5caa1de..e7a5caa1de 100644
--- a/test-suite/bugs/opened/3490.v
+++ b/test-suite/bugs/closed/3490.v
diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v
new file mode 100644
index 0000000000..77427ace58
--- /dev/null
+++ b/test-suite/bugs/closed/3755.v
@@ -0,0 +1,16 @@
+(* File reduced by coq-bug-finder from original input, then from 6729 lines to 
+411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, 
+then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 
+lines to 17 lines *)
+(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml 
+4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk 
+(9e6b28c04ad98369a012faf3bd4d630cf123a473) *)
+Set Printing Universes.
+Section param.
+  Variable typeD : Set -> Set.
+  Variable STex : forall (T : Type) (p : T -> Set), Set.
+  Definition existsEach_cons' v (P : @sigT _ typeD -> Set) :=
+    @STex _ (fun x => P (@existT _ _ v x)).
+
+  Check @existT _ _ STex STex.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
new file mode 100644
index 0000000000..6e19ddf8dc
--- /dev/null
+++ b/test-suite/bugs/closed/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3916.v b/test-suite/bugs/closed/3916.v
new file mode 100644
index 0000000000..55c3a35c3a
--- /dev/null
+++ b/test-suite/bugs/closed/3916.v
@@ -0,0 +1,3 @@
+Require Import List.
+Fail Hint Resolve -> in_map.
+
diff --git a/test-suite/bugs/closed/4016.v b/test-suite/bugs/closed/4016.v
new file mode 100644
index 0000000000..41cb1a8884
--- /dev/null
+++ b/test-suite/bugs/closed/4016.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Parameter eq : relation nat.
+Declare Instance Equivalence_eq : Equivalence eq.
+
+Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x.
+Proof.
+intros z Hz x Hx.
+rewrite <- Hx in Hz.
+destruct z.
+Abort.
+
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
index a6f177b496..aa810f4f0e 100644
--- a/test-suite/bugs/closed/4017.v
+++ b/test-suite/bugs/closed/4017.v
@@ -1,3 +1,5 @@
+Set Implicit Arguments.
+
 (* Use of implicit arguments was lost in multiple variable declarations *)
 Variables 
   (A1 : Type)
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
index c3a045943c..8895e09e02 100644
--- a/test-suite/bugs/closed/4018.v
+++ b/test-suite/bugs/closed/4018.v
@@ -1,3 +1,3 @@
 (* Catching PatternMatchingFailure was lost at some point *)
 Goal nat -> True.
-intros [=].
+Fail intros [=].
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 0000000000..ee84cb94e9
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed export a_subproof.
+Qed export exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index a9aa30df5f..ae6fe7dd0a 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -426,8 +426,9 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depelim' rev tac H :=
-  (try intros until H) ; block_goal ; rev H ;
-  (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
+  (try intros until H) ; block_goal ; 
+  (try revert_until H ; block_goal) ; 
+  generalize_eqs H ; rev H ; tac H ; simpl_dep_elim.
 
 (** 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.  *)
@@ -463,3 +464,9 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :
 
 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" 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" 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/coqc.ml b/tools/coqc.ml
index 5c7be41bec..7e822dbe36 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -121,7 +121,7 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
       as o) :: rem ->
 	begin
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7f435ce960..743cfaccdb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -496,7 +496,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
-  save_proof (Vernacexpr.Proved(true,None));
+  save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =