Merge branch 'v8.5'

29 files changed, 332 insertions, 179 deletions

diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000000..6af0a106ba
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,5 @@
+.dir-locals.el export-ignore
+.gitattributes export-ignore
+.gitignore export-ignore
+.mailmap export-ignore
+TODO export-ignore
diff --git a/CHANGES b/CHANGES
index 19683f8e39..982b96a115 100644
--- a/CHANGES
+++ b/CHANGES
@@ -153,13 +153,14 @@ Tactics
     as existential variables in other goals. To emulate the old
     refine, use "refine c;shelve_unifiable". This can still cause
     incompatibilities in rare occasions.
-  * New "give_up" tactic to skip over a goal without admitting it.
-- The admit tactic has been removed, "give_up" should be used instead.
-  To compile code containing "admit" the following solutions can be adopted:
-  * Add Ltac definition "Ltac admit := give_up." and terminate each
-    incomplete proof with "Admitted".
-  * Add an "Axiom" for each admitted subproof.
-  * Add a single "Axiom proof_admitted : False." and the Ltac definition
+  * New "give_up" tactic to skip over a goal.  A proof containing
+    given up goals cannot be closed with "Qed", but only with "Admitted".
+- The implementation of the admit tactic has changed: no axiom is
+  generated for the admitted sub proof. "admit" is now an alias for
+  "give_up".  Code relying on this specific behavior of "admit"
+  can be made to work by:
+  * Adding an "Axiom" for each admitted subproof.
+  * Adding a single "Axiom proof_admitted : False." and the Ltac definition
     "Ltac admit := case proof_admitted.".
 - Matching using "lazymatch" was fundamentally modified. It now behaves
   like "match" (immediate execution of the matching branch) but without
@@ -215,6 +216,8 @@ Tactics
   on the fly if injection is applicable to the hypothesis under consideration
   (idea borrowed from Georges Gonthier). Introduction pattern [=] applies
   "discriminate" if a discriminable equality.
+- New introduction patterns * and ** to respectively introduce all forthcoming
+  dependent variables and all variables/hypotheses dependent or not.
 - Tactic "injection c as ipats" now clears c if c refers to an
   hypothesis and moves the resulting equations in the hypotheses
   independently of the number of ipats, which has itself to be less
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 2b3862eb08..ab29903b93 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -67,7 +67,7 @@ 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".
+  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
 
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
diff --git a/Makefile.build b/Makefile.build
index 0e3313ecc7..c5b4bbfe85 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -101,12 +101,12 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
 
-ifeq ($(ARCH),Darwin)
+ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin)
 LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
-CODESIGN=codesign -s -
+CODESIGN:=codesign -s -
 else
 LINKMETADATA=
-CODESIGN=true
+CODESIGN:=true
 endif
 
 define bestocaml
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 185c6edfcd..28fdb130e8 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -169,7 +169,15 @@ let sort_cmp univ pb s0 s1 =
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
-        then raise NotConvertible
+        then begin
+          if !Flags.debug then begin
+            let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+            Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+              (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+               ++ Univ.pr_universes univ))
+          end;
+          raise NotConvertible
+        end
     | (_, _) -> raise NotConvertible
 
 let rec no_arg_available = function
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 35f7f14b67..810d6e0b65 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -83,6 +83,7 @@ let import file clib univs digest =
 (* When the module is admitted, digests *must* match *)
 let unsafe_import file clib univs digest =
   let env = !genv in
-  check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
+  if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps
+  else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/votour.ml b/checker/votour.ml
index 29593cb719..d016b45632 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -88,7 +88,7 @@ let rec get_children v o pos = match v with
   |Dyn ->
     let t = to_dyn o in
     let tpe = find_dyn t.dyn_tag in
-    [|(String, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|]
+    [|(Int, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|]
   |Fail s -> failwith "forbidden"
 
 type info = {
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 186bc9add3..d388840df5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1009,7 +1009,7 @@ 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}\comindex{Qed export}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting}
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
@@ -1017,9 +1017,9 @@ From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\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
+unless the proof is ended with ``\texttt{Qed exporting}''.  In such
 case the lemma is preserved.  The syntax
-``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$''
+``\texttt{Qed exporting }\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.
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 854c786c18..159f8df7f2 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,6 +476,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
+    theories/MMaps/MMapFacts.v
+    theories/MMaps/MMapInterface.v
+    theories/MMaps/MMapList.v
+    theories/MMaps/MMapPositive.v
+    theories/MMaps/MMapWeakList.v
+    (theories/MMaps/MMaps.v)
   </dd>
 
   <dt> <b>FSets</b>:
diff --git a/engine/evd.ml b/engine/evd.ml
index 454c51195b..bf519fb7c0 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1189,6 +1189,18 @@ let abstract_undefined_variables uctx =
   in { uctx with uctx_local = Univ.ContextSet.empty;
       uctx_univ_algebraic = vars' }
 
+let fix_undefined_variables ({ universes = uctx } as evm) =
+  let algs', vars' = 
+    Univ.LMap.fold (fun u v (algs, vars as acc) ->
+      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+      else acc)
+      uctx.uctx_univ_variables 
+      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+  in
+    {evm with universes = 
+	{ uctx with uctx_univ_variables = vars';
+	  uctx_univ_algebraic = algs' } }
+
 
 let refresh_undefined_univ_variables uctx =
   let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
diff --git a/engine/evd.mli b/engine/evd.mli
index 0765b951fd..fe785a8314 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -530,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : evar_universe_context -> evar_universe_context
 
+val fix_undefined_variables : evar_map -> evar_map
+
 val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
 
 val nf_constraints : evar_map -> evar_map
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 83be03ffd8..d8f319fa79 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -428,16 +428,20 @@ let rec strengthen_and_subst_mod mb subst mp_from mp_to =
 and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
   match str with
     | [] -> empty_delta_resolver,[]
-    | (l,SFBconst cb) :: rest ->
+    | (l,SFBconst cb) as item :: rest ->
         let cb' = subst_const_body subst cb in
-        let cb'' =
+        let cb' =
           if alias then cb'
           else strengthen_const mp_from l cb' reso
         in
-        let item' = l, SFBconst cb'' in
+        let item' = if cb' == cb then item else (l, SFBconst cb') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
 	if incl then
           (* If we are performing an inclusion we need to add
              the fact that the constant mp_to.l is \Delta-equivalent
@@ -445,26 +449,31 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
           let kn_from = KerName.make2 mp_from l in
           let kn_to = KerName.make2 mp_to l in
           let old_name = kn_of_delta reso kn_from in
-	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
+	  add_kn_delta_resolver kn_to old_name reso', str'
 	else
 	  (* In this case the fact that the constant mp_to.l is
 	     \Delta-equivalent to resolver(mp_from.l) is already known
 	     because reso' contains mp_to maps to reso(mp_from) *)
-	  reso', item'::rest'
-    | (l,SFBmind mib) :: rest ->
-	let item' = l,SFBmind (subst_mind_body subst mib) in
+	  reso', str'
+    | (l,SFBmind mib) as item :: rest ->
+        let mib' = subst_mind_body subst mib in
+        let item' = if mib' == mib then item else (l, SFBmind mib') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
 	(* Same as constant *)
 	if incl then
 	  let kn_from = KerName.make2 mp_from l in
 	  let kn_to = KerName.make2 mp_to l in
 	  let old_name = kn_of_delta reso kn_from in
-	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
+          add_kn_delta_resolver kn_to old_name reso', str'
 	else
-	  reso', item'::rest'
-    | (l,SFBmodule mb) :: rest ->
+          reso', str'
+    | (l,SFBmodule mb) as item :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot (mp_to,l) in
 	let mb' = if alias then
@@ -472,31 +481,39 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
 	else
 	  strengthen_and_subst_mod mb subst mp_from' mp_to'
 	in
-	let item' = l,SFBmodule mb' in
+        let item' = if mb' == mb then item else (l, SFBmodule mb') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
         (* if mb is a functor we should not derive new equivalences
            on names, hence we add the fact that the functor can only
            be equivalent to itself. If we adopt an applicative
            semantic for functor this should be changed.*)
 	if is_functor mb'.mod_type then
-	  add_mp_delta_resolver mp_to' mp_to' reso', item':: rest'
+          add_mp_delta_resolver mp_to' mp_to' reso', str'
 	else
-	  add_delta_resolver reso' mb'.mod_delta, item':: rest'
-    | (l,SFBmodtype mty) :: rest ->
+          add_delta_resolver reso' mb'.mod_delta, str'
+    | (l,SFBmodtype mty) as item :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
-	let mty = subst_modtype subst'
+	let mty' = subst_modtype subst'
 	  (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
           mty
         in
-        let item' = l,SFBmodtype mty in
+        let item' = if mty' == mty then item else (l, SFBmodtype mty') in
 	let reso',rest' =
           strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
-	add_mp_delta_resolver mp_to' mp_to' reso', item'::rest'
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
+	add_mp_delta_resolver mp_to' mp_to' reso', str'
 
 
 (** Let P be a module path when we write:
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 63def9a1dc..a5e8fb9c2b 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -47,3 +47,5 @@ let tag (s,_) =
     anomaly msg
 
 let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+
+let dump () = Int.Map.bindings !dyntab
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 4a7134721c..cac912aca1 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -14,3 +14,4 @@ val create : string -> ('a -> t) * (t -> 'a)
 val tag : t -> string
 val has_tag : t -> string -> bool
 val pointer_equal : t -> t -> bool
+val dump : unit -> (int * string) list
diff --git a/library/library.ml b/library/library.ml
index 7513cf8387..2b607e1a38 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -17,6 +17,59 @@ open Libobject
 open Lib
 
 (************************************************************************)
+(*s Low-level interning/externing of libraries to files *)
+
+(*s Loading from disk to cache (preparation phase) *)
+
+let (raw_extern_library, raw_intern_library) =
+  System.raw_extern_intern Coq_config.vo_magic_number
+
+(************************************************************************)
+(** Serialized objects loaded on-the-fly *)
+
+exception Faulty of string
+
+module Delayed :
+sig
+
+type 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed
+val fetch_delayed : 'a delayed -> 'a
+
+end =
+struct
+
+type 'a delayed = {
+  del_file : string;
+  del_off : int;
+  del_digest : Digest.t;
+}
+
+let in_delayed f ch =
+  let pos = pos_in ch in
+  let _, digest = System.skip_in_segment f ch in
+  { del_file = f; del_digest = digest; del_off = pos; }
+
+(** Fetching a table of opaque terms at position [pos] in file [f],
+    expecting to find first a copy of [digest]. *)
+
+let fetch_delayed del =
+  let { del_digest = digest; del_file = f; del_off = pos; } = del in
+  try
+    let ch = System.with_magic_number_check raw_intern_library f in
+    let () = seek_in ch pos in
+    let obj, _, digest' = System.marshal_in_segment f ch in
+    let () = close_in ch in
+    if not (String.equal digest digest') then raise (Faulty f);
+    obj
+  with e when Errors.noncritical e -> raise (Faulty f)
+
+end
+
+open Delayed
+
+
+(************************************************************************)
 (*s Modules on disk contain the following informations (after the magic
     number, and before the digest). *)
 
@@ -42,12 +95,19 @@ type library_t = {
   library_extra_univs : Univ.universe_context_set;
 }
 
+type library_summary = {
+  libsum_name : compilation_unit_name;
+  libsum_digests : Safe_typing.vodigest;
+  libsum_imports : compilation_unit_name array;
+}
+
 module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
-let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
+let libraries_table : library_summary LibraryMap.t ref =
+  Summary.ref LibraryMap.empty ~name:"LIBRARY"
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
@@ -89,32 +149,31 @@ let library_is_loaded dir =
   with Not_found -> false
 
 let library_is_opened dir =
-  List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list
+  List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list
 
-let loaded_libraries () =
-  List.map (fun m -> m.library_name) !libraries_loaded_list
+let loaded_libraries () = !libraries_loaded_list
 
-let opened_libraries () =
-  List.map (fun m -> m.library_name) !libraries_imports_list
+let opened_libraries () = !libraries_imports_list
 
   (* If a library is loaded several time, then the first occurrence must
      be performed first, thus the libraries_loaded_list ... *)
 
 let register_loaded_library m =
+  let libname = m.libsum_name in
   let link m =
-    let dirname = Filename.dirname (library_full_filename m.library_name) in
-    let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in
+    let dirname = Filename.dirname (library_full_filename libname) in
+    let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
     if not !Flags.no_native_compiler then
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
-    | [] -> link m; [m]
-    | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l
+    | [] -> link m; [libname]
+    | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
-  libraries_table := LibraryMap.add m.library_name m !libraries_table
+  libraries_table := LibraryMap.add libname m !libraries_table
 
   (* ... while if a library is imported/exported several time, then
      only the last occurrence is really needed - though the imported
@@ -125,7 +184,7 @@ let register_loaded_library m =
 let rec remember_last_of_each l m =
   match l with
   | [] -> [m]
-  | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m
+  | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m
   | m'::l' -> m' :: remember_last_of_each l' m
 
 let register_open_library export m =
@@ -139,17 +198,15 @@ let register_open_library export m =
 (* [open_library export explicit m] opens library [m] if not already
    opened _or_ if explicitly asked to be (re)opened *)
 
-let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name
-
 let open_library export explicit_libs m =
   if
     (* Only libraries indirectly to open are not reopen *)
     (* Libraries explicitly mentionned by the user are always reopen *)
-    List.exists (eq_lib_name m) explicit_libs
-    || not (library_is_opened m.library_name)
+    List.exists (fun m' -> DirPath.equal m m') explicit_libs
+    || not (library_is_opened m)
   then begin
     register_open_library export m;
-    Declaremods.really_import_module (MPfile m.library_name)
+    Declaremods.really_import_module (MPfile m)
   end
   else
     if export then
@@ -164,11 +221,12 @@ let open_libraries export modl =
       (fun l m ->
          let subimport =
            Array.fold_left
-             (fun l m -> remember_last_of_each l (try_find_library m))
-             l m.library_imports
-         in remember_last_of_each subimport m)
+             (fun l m -> remember_last_of_each l m)
+             l m.libsum_imports
+         in remember_last_of_each subimport m.libsum_name)
       [] modl in
-  List.iter (open_library export modl) to_open_list
+  let explicit = List.map (fun m -> m.libsum_name) modl in
+  List.iter (open_library export explicit) to_open_list
 
 
 (**********************************************************************)
@@ -201,14 +259,6 @@ let in_import_library : DirPath.t list * bool -> obj =
 
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
-
-(*s Loading from disk to cache (preparation phase) *)
-
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
-
-(************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
 exception LibUnmappedDir
@@ -300,34 +350,10 @@ let try_locate_qualified_library (loc,qid) =
     terms, and access them only when a specific command (e.g. Print or
     Print Assumptions) needs it. *)
 
-exception Faulty
-
-(** Fetching a table of opaque terms at position [pos] in file [f],
-    expecting to find first a copy of [digest]. *)
-
-let fetch_table what dp (f,pos,digest) =
-  let dir_path = Names.DirPath.to_string dp in
-  try
-    msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
-    let ch = System.with_magic_number_check raw_intern_library f in
-    let () = seek_in ch pos in
-    if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
-    let table, pos', digest' = System.marshal_in_segment f ch in
-    let () = close_in ch in
-    let ch' = open_in_bin f in
-    if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty;
-    let () = close_in ch' in
-    table
-  with e when Errors.noncritical e ->
-    error
-      ("The file "^f^" (bound to " ^ dir_path ^
-      ") is inaccessible or corrupted,\n" ^
-      "cannot load some "^what^" in it.\n")
-
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of string * int * Digest.t
+  | ToFetch of 'a Future.computation array delayed
   | Fetched of 'a Future.computation array
 
 let opaque_tables =
@@ -340,25 +366,33 @@ let add_opaque_table dp st =
 let add_univ_table dp st =
   univ_tables := LibraryMap.add dp st !univ_tables
 
-let access_table fetch_table add_table tables dp i =
-  let t = match LibraryMap.find dp tables with
+let access_table what tables dp i =
+  let t = match LibraryMap.find dp !tables with
     | Fetched t -> t
-    | ToFetch (f,pos,digest) ->
-      let t = fetch_table dp (f,pos,digest) in
-      add_table dp (Fetched t);
+    | ToFetch f ->
+      let dir_path = Names.DirPath.to_string dp in
+      msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      let t =
+        try fetch_delayed f
+        with Faulty f ->
+          error
+            ("The file "^f^" (bound to " ^ dir_path ^
+            ") is inaccessible or corrupted,\n" ^
+            "cannot load some "^what^" in it.\n")
+      in
+      tables := LibraryMap.add dp (Fetched t) !tables;
       t
   in
   assert (i < Array.length t); t.(i)
 
 let access_opaque_table dp i =
-  access_table
-    (fetch_table "opaque proofs")
-    add_opaque_table !opaque_tables dp i
+  let what = "opaque proofs" in
+  access_table what opaque_tables dp i
+
 let access_univ_table dp i =
   try
-    Some (access_table 
-            (fetch_table "universe contexts of opaque proofs")
-            add_univ_table !univ_tables dp i)
+    let what = "universe contexts of opaque proofs" in
+    Some (access_table what univ_tables dp i)
   with Not_found -> None
 
 let () =
@@ -385,15 +419,22 @@ let mk_library md digests univs =
     library_extra_univs = univs;
   }
 
+let mk_summary m = {
+  libsum_name = m.library_name;
+  libsum_imports = m.library_imports;
+  libsum_digests = m.library_digests;
+}
+
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
   let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let pos, digest = System.skip_in_segment f ch in
+  let _ = System.skip_in_segment f ch in
+  let (del_opaque : seg_proofs delayed) = in_delayed f ch in
   close_in ch;
   register_library_filename lmd.md_name f;
-  add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
+  add_opaque_table lmd.md_name (ToFetch del_opaque);
   let open Safe_typing in
   match univs with
   | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
@@ -409,10 +450,10 @@ module DPMap = Map.Make(DirPath)
 let rec intern_library (needed, contents) (dir, f) from =
   Pp.feedback(Feedback.FileDependency (from, f));
   (* Look if in the current logical environment *)
-  try find_library dir, (needed, contents)
+  try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
-  try DPMap.find dir contents, (needed, contents)
+  try (DPMap.find dir contents).library_digests, (needed, contents)
   with Not_found ->
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
   let m = intern_from_file f in
@@ -422,15 +463,15 @@ let rec intern_library (needed, contents) (dir, f) from =
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
-  m, intern_library_deps (needed, contents) dir m (Some f)
+  m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
 
 and intern_library_deps libs dir m from =
   let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
 and intern_mandatory_library caller from libs (dir,d) =
-  let m, libs = intern_library libs (try_locate_absolute_library dir) from in
-  if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then
+  let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
+  if not (Safe_typing.digest_match ~actual:digest ~required:d) then
     errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
       ".vo makes inconsistent assumptions over library " ^
       DirPath.to_string dir));
@@ -501,7 +542,7 @@ let register_library m =
     m.library_objects
     m.library_digests
     m.library_extra_univs;
-  register_loaded_library m
+  register_loaded_library (mk_summary m)
 
 (* Follow the semantics of Anticipate object:
    - called at module or module type closing when a Require occurs in
@@ -667,10 +708,13 @@ let load_library_todo f =
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
 
 let current_deps () =
-  List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list
+  let map name =
+    let m = try_find_library name in
+    (name, m.libsum_digests)
+  in
+  List.map map !libraries_loaded_list
 
-let current_reexports () =
-  List.map (fun m -> m.library_name) !libraries_exports_list
+let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
   errorlabstrm ""
@@ -766,11 +810,7 @@ let save_library_raw f lib univs proofs =
 
 open Printf
 
-let mem s =
-  let m = try_find_library s in
-  h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
-		 (CObj.size_kb m) (CObj.size_kb m.library_compiled)
-		 (CObj.size_kb m.library_objects)))
+let mem s = Pp.mt ()
 
 module StringOrd = struct type t = string let compare = String.compare end
 module StringSet = Set.Make(StringOrd)
@@ -778,7 +818,7 @@ module StringSet = Set.Make(StringOrd)
 let get_used_load_paths () =
   StringSet.elements
     (List.fold_left (fun acc m -> StringSet.add
-      (Filename.dirname (library_full_filename m.library_name)) acc)
+      (Filename.dirname (library_full_filename m)) acc)
        StringSet.empty !libraries_loaded_list)
 
 let _ = Nativelib.get_load_paths := get_used_load_paths
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index b23841ceff..1e254c16ba 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -53,7 +53,7 @@ GEXTEND Gram
 	  VernacSolveExistential (n,c)
       | IDENT "Admitted" -> VernacEndProof Admitted
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
-      | IDENT "Qed"; IDENT "export"; l = LIST0 identref SEP "," ->
+      | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
       | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 90ee6d0ef1..5ea4fb763e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -440,7 +440,8 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
+  let p = d.file_naming mp ^ d.file_suffix in
+  Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5e08fef5fe..52459f78eb 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
-  [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
+  [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
@@ -56,11 +56,14 @@ let preamble mod_name comment used_modules usf =
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nimport qualified GHC.Prim\
+\ntype Any = GHC.Prim.Any\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
 \nimport qualified IOExts\
+\ntype Any = ()\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
@@ -102,7 +105,7 @@ let rec pp_type par vl t =
 	pp_par par
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
-    | Tunknown -> str "()"
+    | Tunknown -> str "Any"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
  in
   hov 0 (pp_rec par t)
@@ -243,12 +246,12 @@ let pp_logical_ind packet =
 	      prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet =
+  let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
-  let l' = List.rev l in
-  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
+  hov 2 (str "type " ++ name ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
 	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
-	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
@@ -360,6 +363,7 @@ let pp_struct =
 let haskell_descr = {
   keywords = keywords;
   file_suffix = ".hs";
+  file_naming = string_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 1e491d36f7..b7dee6cb14 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -197,6 +197,7 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
+  file_naming : module_path -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
     Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 85f18a0933..8c482b4b1d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -746,6 +746,7 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 let ocaml_descr = {
   keywords = keywords;
   file_suffix = ".ml";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = Some ".mli";
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 69dea25aac..99b4fd448d 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -225,6 +225,7 @@ let pp_struct =
 let scheme_descr = {
   keywords = keywords;
   file_suffix = ".scm";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2917f52c58..5bff3c8131 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -295,7 +295,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 	let ctx = Evd.evar_universe_context_set universes in
         if keep_body_ucst_sepatate then
           (* For vi2vo compilation proofs are computed now but we need to
-           * completent the univ constraints of the typ with the ones of
+           * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
           let ctx_body = restrict_universe_context ctx used_univs_body in
           let ctx_typ = restrict_universe_context ctx used_univs_typ in
diff --git a/stm/stm.ml b/stm/stm.ml
index 70e242bb54..d9ecc8bcce 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,7 +8,8 @@
 
 let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err s end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
 
 open Vernacexpr
 open Errors
@@ -1601,10 +1602,11 @@ let pstate = summary_pstate
 
 let async_policy () =
   let open Flags in
-  if interactive () = `Yes then
-    (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy)
+  if is_universe_polymorphism () then false
+  else if interactive () = `Yes then
+    (async_proofs_is_master () || !async_proofs_mode = APonLazy)
   else
-    (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff)
+    (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
 
 let delegate name =
   let time = get_hint_bp_time name in
@@ -1632,12 +1634,17 @@ let collect_proof keep cur hd brkind id =
  let has_proof_no_using = function
    | Some (_, { expr = VernacProof(_,None) }) -> true
    | _ -> false in
+ let may_pierce_opaque = function
+   | { expr = VernacPrint (PrintName _) } -> true
+   | _ -> false in
  let parent = function Some (p, _) -> p | None -> assert false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
+    | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
+      when may_pierce_opaque x -> `Sync(no_name,None,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
-    | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
     | `Alias _ -> `Sync (no_name,None,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
@@ -1657,7 +1664,9 @@ let collect_proof keep cur hd brkind id =
           let t, v = proof_no_using last in
           v.expr <- VernacProof(t, Some hint);
           `ASync (parent last,proof_using_ast last,accn,name,delegate name)
-        with Not_found -> `Sync (no_name,None,`NoHint))
+        with Not_found ->
+          let name = name ids in
+          `MaybeASync (parent last, None, accn, name, delegate name))
     | `Fork((_, hd', GuaranteesOpacity, ids), _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
@@ -1684,16 +1693,27 @@ let collect_proof keep cur hd brkind id =
        else make_sync `AlreadyEvaluated rc
 
 let string_of_reason = function
-  | `Transparent -> "Transparent"
-  | `AlreadyEvaluated -> "AlreadyEvaluated"
-  | `Policy -> "Policy"
-  | `NestedProof -> "NestedProof"
-  | `Immediate -> "Immediate"
-  | `Alias -> "Alias"
-  | `NoHint -> "NoHint"
-  | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
-  | `Aborted -> "Aborted"
-  | _ -> "Unknown Reason"
+  | `Transparent -> "non opaque"
+  | `AlreadyEvaluated -> "proof already evaluated"
+  | `Policy -> "policy"
+  | `NestedProof -> "contains nested proof"
+  | `Immediate -> "proof term given explicitly"
+  | `Aborted -> "aborted proof"
+  | `Doesn'tGuaranteeOpacity -> "not a simple opaque lemma"
+  | `MutualProofs -> "block of mutually recursive proofs"
+  | `Alias -> "contains Undo-like command"
+  | `Print -> "contains Print-like command"
+  | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
+  | `Unknown -> "unsupported case"
+
+let log_string s = prerr_debug ("STM: " ^ s)
+let log_processing_async id name = log_string Printf.(sprintf
+  "%s: proof %s: asynch" (Stateid.to_string id) name
+)
+let log_processing_sync id name reason = log_string Printf.(sprintf
+  "%s: proof %s: synch (cause: %s)"
+  (Stateid.to_string id) name (string_of_reason reason)
+)
 
 let wall_clock_last_fork = ref 0.0
 
@@ -1758,7 +1778,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 assert(keep == VtKeep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
                 let stop, exn_info, loc = eop, (id, eop), x.loc in
-                prerr_endline ("Asynchronous " ^ Stateid.to_string id);
+                log_processing_async id name;
                 VCS.create_cluster nodes ~qed:id ~start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
@@ -1796,8 +1816,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 reach eop; vernac_interp id x; Proof_global.discard_all ()
               ), `Yes, true
           | `Sync (name, pua, reason) -> (fun () ->
-                prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
-                  string_of_reason reason);
+                log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
                 record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
@@ -1823,12 +1842,11 @@ let known_state ?(redefine_qed=false) ~cache id =
                 Proof_global.discard_all ()
               ), `Yes, true
           | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
-                prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
                 reach ~cache:`Shallow start;
                 (* no sections *)
                 if List.is_empty (Environ.named_context (Global.env ()))
                 then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
-                else pi1 (aux (`Sync (name, pua, `Unknown))) ()
+                else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
               ), (if redefine_qed then `No else `Yes), true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
@@ -1885,9 +1903,16 @@ let observe id =
     iraise e
 
 let finish ?(print_goals=false) () =
-  observe (VCS.get_branch_pos (VCS.current_branch ()));
+  let head = VCS.current_branch () in
+  observe (VCS.get_branch_pos head);
   if print_goals then msg_notice (pr_open_cur_subgoals ());
-  VCS.print ()
+  VCS.print ();
+  (* Some commands may by side effect change the proof mode *)
+  match VCS.get_branch head with
+  | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+  | _ -> ()
+
 
 let wait () =
   Slaves.wait_all_done ();
@@ -2356,7 +2381,7 @@ let interp verb (_,e as lexpr) =
       verb && match clas with
        | VtQuery _, _ -> false
        | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
-       | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
+       | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
       let e = Errors.push e in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 81fad13793..783ff2e116 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -65,6 +65,11 @@ let rec classify_vernac e =
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
       when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
+    (* Univ poly compatibility: we run it now, so that we can just
+     * look at Flags in stm.ml.  Would be nicer to have the stm
+     * look at the entire dag to detect this option. *)
+    | VernacSetOption (["Universe"; "Polymorphism"],_)
+    | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
     (* Stm *)
     | VernacStm Finish -> VtStm (VtFinish, true), VtNow
     | VernacStm Wait -> VtStm (VtWait, true), VtNow
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 6d3dc461ec..e909a14c9e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -196,6 +196,12 @@ TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
 
+(* Admit *)
+
+TACTIC EXTEND admit
+ [ "admit" ] -> [ Proofview.give_up ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
index ee84cb94e9..b3e41ab1fb 100644
--- a/test-suite/success/qed_export.v
+++ b/test-suite/success/qed_export.v
@@ -3,8 +3,8 @@ Proof.
 assert True as H.
   abstract (trivial) using exported_seff.
 exact H.
-Fail Qed export a_subproof.
-Qed export exported_seff.
+Fail Qed exporting a_subproof.
+Qed exporting exported_seff.
 Check ( exported_seff : True ).
 
 Lemma b : True.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 1e0bfacf93..cf9b8a087d 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -46,8 +46,8 @@ let section s =
 let usage () =
   output_string stderr "Usage summary:
 
-coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
-  [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
+coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]
+  ... [any] ... [-extra[-phony] result dependencies command]
   ... [-I dir] ... [-R physicalpath logicalpath]
   ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
   ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
@@ -57,8 +57,8 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
 [file.ml[i4]?]: Objective Caml file to be compiled
 [file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
   library/module
-[subdirectory] : subdirectory that should be \"made\" and has a
-  Makefile itself to do so.
+[any] : subdirectory that should be \"made\" and has a Makefile itself
+  to do so. Very fragile and discouraged.
 [-extra result dependencies command]: add target \"result\" with command
   \"command\" and dependencies \"dependencies\". If \"result\" is not
   generic (do not contains a %), \"result\" is built by _make all_ and
@@ -344,6 +344,10 @@ let clean sds sps =
     (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n")
     sds;
   print "\n";
+  let () =
+    if !some_vfile then
+      let () = print "cleanall:: clean\n" in
+      print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in
   print "archclean::\n";
   print "\trm -f *.cmx *.o\n";
   List.iter
@@ -545,7 +549,12 @@ let subdirs sds =
   let pr_subdir s =
     print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n"
   in
-    if sds <> [] then section "Subdirectories.";
+  if sds <> [] then
+    let () =
+      Format.eprintf "@[Warning: Targets for subdirectories are very fragile.@ " in
+    let () =
+      Format.eprintf "For example,@ nothing is done to handle dependencies@ with them.@]@." in
+      section "Subdirectories.";
     List.iter pr_subdir sds
 
 let forpacks l =
@@ -697,25 +706,25 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     end
 
 let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
-  let other_targets = CList.map_filter
-    (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
-    sps @ sds in
+  let other_targets =
+    CList.map_filter
+      (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
+      sps @ sds in
   main_targets vfiles mlfiles other_targets inc;
-    print ".PHONY: ";
-    print_list " "
-      ("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)));
-    print "\n\n";
-    custom sps;
-    subdirs sds;
-    forpacks mlpackfiles
+  print ".PHONY: ";
+  print_list
+    " "
+    ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall"
+     :: "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)));
+  print "\n\n";
+  custom sps;
+  subdirs sds;
+  forpacks mlpackfiles
 
 let banner () =
   print (Printf.sprintf
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e9b5e8f84a..6909d89440 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -67,6 +67,7 @@ let print_usage_channel co command =
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
+\n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
 \n  -no-native-compiler    disable the native_compute reduction machinery\
 \n  -h, -help              print this list of options\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 52b4dc8cf6..a4ffae0fff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1952,14 +1952,16 @@ let interp ?proof locality poly c =
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
   | VernacNop -> ()
 
+  (* The STM should handle that, but LOAD bypasses the STM... *)
+  | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
+  | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm")
+  | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm")
+  | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm")
+  | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm")
+  | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
+  
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
-  | VernacAbort id -> anomaly (str "VernacAbort not handled by Stm")
-  | VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm")
-  | VernacRestart -> anomaly (str "VernacRestart not handled by Stm")
-  | VernacUndo _ -> anomaly (str "VernacUndo not handled by Stm")
-  | VernacUndoTo _ -> anomaly (str "VernacUndoTo not handled by Stm")
-  | VernacBacktrack _ -> anomaly (str "VernacBacktrack not handled by Stm")
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()