31 files changed, 244 insertions, 184 deletions
diff --git a/CHANGES b/CHANGES
index acf393b9c..8564b1d31 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,8 +61,9 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
-- The -require command-line option now takes a logical path of a given library
-  rather than a physical path.
+- The -require and -load-vernac-object command-line options now take a logical
+  path of a given library rather than a physical path, thus they behave like
+  Require [Import] path.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/Makefile.build b/Makefile.build
index d8c8ba4e8..c554adadb 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -525,7 +525,7 @@ hightactics: tactics/hightactics.cma
 .PHONY: init theories theories-light
 .PHONY: logic arith bool narith zarith qarith lists strings sets
 .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
-.PHONY: msets mmaps
+.PHONY: msets mmaps compat
 
 init: $(INITVO)
 
@@ -555,6 +555,7 @@ structures: $(STRUCTURESVO)
 vectors: $(VECTORSVO)
 msets: $(MSETSVO)
 mmaps: $(MMAPSVO)
+compat: $(COMPATVO)
 
 noreal: unicode logic arith bool zarith qarith lists sets fsets \
 	relations wellfounded setoids sorting
diff --git a/Makefile.common b/Makefile.common
index f6ec1694a..1bc09b9ba 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -302,6 +302,7 @@ SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids)
 UNICODEVO:=$(call cat_vo_itarget, theories/Unicode)
 CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
 PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
+COMPATVO:=$(call cat_vo_itarget, theories/Compat)
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
@@ -311,7 +312,8 @@ THEORIESVO:=\
   $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
   $(SETSVO) $(FSETSVO) $(MSETSVO) $(MMAPSVO) \
   $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO)
+  $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \
+  $(COMPATVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)
 
diff --git a/checker/check.ml b/checker/check.ml
index c835cec82..2bc470aea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -271,20 +271,10 @@ let try_locate_qualified_library qid =
     | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
+(*s Low-level interning of libraries from files *)
 
-(*s Loading from disk to cache (preparation phase) *)
-
-let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number)
-
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let raw_intern_library f =
+  System.raw_intern_state Coq_config.vo_magic_number f
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -312,7 +302,7 @@ let intern_from_file (dir, f) =
   Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
   let (sd,md,table,opaque_csts,digest) =
     try
-      let ch = with_magic_number_check raw_intern_library f in
+      let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
       let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
       let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 0f1823a02..9862abb53 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
   standard input.
 
-\item[{\tt -load-vernac-object} {\em file}]\ 
+\item[{\tt -load-vernac-object} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo}
+  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
 
 \item[{\tt -require} {\em path}]\ 
 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index c8d05013b..c6fbd1c53 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -215,12 +215,13 @@ mouse button, press the key you want for the new shortcut, and release
 the mouse button afterwards. If your system does not allow it, you may still 
 edit this configuration file by hand, but this is more involved.
 
-\section{Using unicode symbols}
+\section{Using Unicode symbols}
 
-\CoqIDE{} supports unicode character encoding in its text windows,
-consequently a large set of symbols is available for notations.
+\CoqIDE{} is based on GTK+ and inherits from it support for Unicode in
+its text windows. Consequently a large set of symbols is available for
+notations.
 
-\subsection{Displaying unicode symbols}
+\subsection{Displaying Unicode symbols}
 
 You just need to define suitable notations as described in
 Chapter~\ref{Addoc-syntax}. For example, to use the mathematical symbols
@@ -236,31 +237,33 @@ file \verb|utf8.v| of \Coq{} library, so you may enable them just by
 \verb|Require utf8| inside \CoqIDE{}, or equivalently, by starting
 \CoqIDE{} with \verb|coqide -l utf8|.
 
-However, there are some issues when using such unicode symbols: you of
+However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts
-section of the preferences, the Preview line displays some unicode symbols, so
+section of the preferences, the Preview line displays some Unicode symbols, so
 you could figure out if the selected font is OK. Related to this, one
-thing you may need to do is choose whether Gtk should use antialiased
+thing you may need to do is choose whether GTK+ should use antialiased
 fonts or not, by setting the environment variable \verb|GDK_USE_XFT|
 to 1 or 0 respectively.
 
 \subsection{Defining an input method for non ASCII symbols}
 
-To input an Unicode symbol, a general method is to press both the
-CONTROL and the SHIFT keys, and type the hexadecimal code of the
+To input a Unicode symbol, a general method provided by GTK+
+is to simultaneously press the
+Control, Shift and ``u'' keys, release, then type the hexadecimal code of the
 symbol required, for example \verb|2200| for the $\forall$ symbol.
 A list of symbol codes is available at \url{http://www.unicode.org}. 
 
-This method obviously doesn't scale, that's why the preferred alternative is to
-use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
-MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
+An alternative method which does not require to know the hexadecimal
+code of the character is to use an Input Method Editor. On POSIX
+systems (Linux distributions, BSD variants and MacOS X), you can use
+\texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
 input method.
 
 To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
 In the "Global Settings" group set the default Input Method to "ELatin" (don't
 forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
 layout to "TeX", and remember the content of the "[ELatin] on" field (by default
-"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming
+Control-\textbackslash). You can now execute CoqIDE with the following commands (assuming
 you use a Bourne-style shell):
 
 \begin{verbatim}
@@ -268,7 +271,7 @@ $ export GTK_IM_MODULE=uim
 $ coqide
 \end{verbatim}
 
-Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
+Activate the ELatin Input Method with Control-\textbackslash, then type the
 sequence "\verb=\Gamma=". You will see the sequence being
 replaced by $\Gamma$ as soon as you type the second "a".
 
@@ -286,7 +289,7 @@ detect its character encoding.)
 If you choose something else than UTF-8, then missing characters will
 be written encoded by \verb|\x{....}| or \verb|\x{........}| where
 each dot is an hexadecimal digit: the number between braces is the
-hexadecimal UNICODE index for the missing character.
+hexadecimal Unicode index for the missing character.
 
 
 %%% Local Variables: 
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index ee2b042f4..26dbd59e7 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -285,7 +285,7 @@ suffix \verb!.tex!.
   
   Select a \texmacs\ output.
 
-\item[\texttt{--stdout}] ~\par
+\item[\texttt{\mm{}stdout}] ~\par
 
   Write output to stdout.
 
@@ -496,14 +496,25 @@ Default behavior is to assume ASCII 7 bits input files.
 \item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par
 
   Select ISO-8859-1 input files. It is equivalent to
-  \texttt{--inputenc latin1 --charset iso-8859-1}.
+  \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}.
 
 \item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par
 
-  Select UTF-8 (Unicode) input files. It is equivalent to
-  \texttt{--inputenc utf8 --charset utf-8}.
-  \LaTeX\ UTF-8 support can be found at
- \url{http://www.ctan.org/pkg/unicode}.
+  Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and
+  \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode
+  replacements for a couple of standard plain ASCII notations such
+  as $\rightarrow$ for \texttt{->} and $\forall$ for
+  \texttt{forall}. \LaTeX\ UTF-8 support can be found at
+  \url{http://www.ctan.org/pkg/unicode}.
+
+  For the interpretation of Unicode characters by \LaTeX, extra
+  packages which {\coqdoc} does not provide by default might be
+  required, such as \texttt{textgreek} for some Greek letters or
+  \texttt{stmaryrd} for some mathematical symbols. If a Unicode
+  character is missing an interpretation in the \texttt{utf8x} input
+  encoding, add
+  \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages
+  and declarations can be added with option \texttt{-p}.
 
 \item[\texttt{\mm{}inputenc} \textit{string}] ~\par
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 12a04fcc2..2fdf3699f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1378,7 +1378,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
-  extras = Store.empty;
+  extras = evd.extras;
 }
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/lib/pp.ml b/lib/pp.ml
index 01df2510c..51bd70a49 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -424,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit
 let make_body info s =
   emacs_quote (hov 0 (info ++ spc () ++ s))
 
-let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm)
+let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm))
 let warnbody strm = make_body (str "Warning:") strm
 let errorbody strm = make_body (str "Error:") strm
 let infobody strm = emacs_quote_info strm
diff --git a/lib/system.ml b/lib/system.ml
index e4a60eccb..7a62d5603 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -215,48 +215,42 @@ let skip_in_segment f ch =
 
 exception Bad_magic_number of string
 
-let raw_extern_intern magic =
-  let extern_state filename =
-    let channel = open_trapping_failure filename in
-    output_binary_int channel magic;
-    filename, channel
-  and intern_state filename =
-    try
-      let channel = open_in_bin filename in
-      if not (Int.equal (input_binary_int filename channel) magic) then
-        raise (Bad_magic_number filename);
-      channel
-    with
-    | End_of_file -> error_corrupted filename "premature end of file"
-    | Failure s | Sys_error s -> error_corrupted filename s
-  in
-  (extern_state,intern_state)
+let raw_extern_state magic filename =
+  let channel = open_trapping_failure filename in
+  output_binary_int channel magic;
+  channel
 
-let extern_intern ?(warn=true) magic =
-  let (raw_extern,raw_intern) = raw_extern_intern magic in
-  let extern_state name val_0 =
-    try
-      let (filename,channel) = raw_extern name in
-      try
-        marshal_out channel val_0;
-        close_out channel
-      with reraise ->
-	let reraise = Errors.push reraise in
-        let () = try_remove filename in
-        iraise reraise
-    with Sys_error s ->
-      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
-  and intern_state paths name =
+let raw_intern_state magic filename =
+  try
+    let channel = open_in_bin filename in
+    if not (Int.equal (input_binary_int filename channel) magic) then
+      raise (Bad_magic_number filename);
+    channel
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted filename s
+
+let extern_state magic filename val_0 =
+  try
+    let channel = raw_extern_state magic filename in
     try
-      let _,filename = find_file_in_path ~warn paths name in
-      let channel = raw_intern filename in
-      let v = marshal_in filename channel in
-      close_in channel;
-      v
-    with Sys_error s ->
-      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
-  in
-  (extern_state,intern_state)
+      marshal_out channel val_0;
+      close_out channel
+    with reraise ->
+      let reraise = Errors.push reraise in
+      let () = try_remove filename in
+      iraise reraise
+  with Sys_error s ->
+    errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+
+let intern_state magic filename =
+  try
+    let channel = raw_intern_state magic filename in
+    let v = marshal_in filename channel in
+    close_in channel;
+    v
+  with Sys_error s ->
+    errorlabstrm "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
diff --git a/lib/system.mli b/lib/system.mli
index 6ed450326..2e773fe96 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -66,11 +66,13 @@ val find_file_in_path :
 
 exception Bad_magic_number of string
 
-val raw_extern_intern : int ->
-  (string -> string * out_channel) * (string -> in_channel)
+val raw_extern_state : int -> string -> out_channel
 
-val extern_intern : ?warn:bool -> int ->
-  (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a)
+val raw_intern_state : int -> string -> in_channel
+
+val extern_state : int -> string -> 'a -> unit
+
+val intern_state : int -> string -> 'a
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
diff --git a/library/library.ml b/library/library.ml
index a09f91b15..024ac9e6f 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -19,10 +19,12 @@ open Lib
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
 
-(*s Loading from disk to cache (preparation phase) *)
+let raw_extern_library f =
+  System.raw_extern_state Coq_config.vo_magic_number f
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
+let raw_intern_library f =
+  System.with_magic_number_check
+    (System.raw_intern_state Coq_config.vo_magic_number) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -56,7 +58,7 @@ let in_delayed f ch =
 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 ch = 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
@@ -434,7 +436,7 @@ let mk_summary m = {
 }
 
 let intern_from_file f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
   let (lmd : seg_lib delayed) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
@@ -488,33 +490,11 @@ let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let rec_intern_by_filename_only f =
-  let m = try intern_from_file f with Sys_error s -> error s in
-  (* We check no other file containing same library is loaded *)
-  if library_is_loaded m.library_name then
-    begin
-      msg_warning
-	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
-	str (library_full_filename m.library_name));
-      m.library_name, []
-    end
- else
-    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in
-    let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in
-    m.library_name, needed
-
 let native_name_from_filename f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file f =
-  (* A name is specified, we have to check it contains library id *)
-  let paths = Loadpath.get_paths () in
-  let _, f =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only f
-
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
@@ -590,18 +570,6 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file file export =
-  let modref,needed = rec_intern_library_from_file file in
-  let needed = List.rev_map snd needed in
-  if Lib.is_module_or_modtype () then begin
-    add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp)))
-      export
-  end
-  else
-    add_anonymous_leaf (in_require (needed,[modref],export));
-  add_frozen_state ()
-
 (* the function called by Vernacentries.vernac_import *)
 
 let safe_locate_module (loc,qid) =
@@ -686,11 +654,9 @@ let start_library f =
   ldir
 
 let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
@@ -778,7 +744,8 @@ let save_library_to ?todo dir f otab =
   if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
     error_recursively_dependent_library dir;
   (* Open the vo file and write the magic number *)
-  let (f',ch) = raw_extern_library f in
+  let f' = f in
+  let ch = raw_extern_library f' in
   try
     (* Writing vo payload *)
     System.marshal_out_segment f' ch (sd           : seg_sum);
@@ -801,7 +768,8 @@ let save_library_to ?todo dir f otab =
     iraise reraise
 
 let save_library_raw f sum lib univs proofs =
-  let (f',ch) = raw_extern_library (f^"o") in
+  let f' = f^"o" in
+  let ch = raw_extern_library f' in
   System.marshal_out_segment f' ch (sum        : seg_sum);
   System.marshal_out_segment f' ch (lib        : seg_lib);
   System.marshal_out_segment f' ch (Some univs : seg_univ option);
diff --git a/library/library.mli b/library/library.mli
index 3d96f9a75..d5e610dd6 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,7 +22,6 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file : CUnix.physical_path -> bool option -> unit
 
 (** {6 Start the compilation of a library } *)
 
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e7..622d390a2 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -28,8 +28,6 @@ let physical p = p.path_physical
 
 let get_load_paths () = !load_paths
 
-let get_paths () = List.map physical !load_paths
-
 let anomaly_too_many_paths path =
   anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
 
@@ -112,3 +110,9 @@ let expand_path dir =
       if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
   in
   aux !load_paths
+
+let locate_file fname =
+  let paths = List.map physical !load_paths in
+  let _,longfname =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+  longfname
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 3251b8c60..269e28e0b 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -27,9 +27,6 @@ val logical : t -> DirPath.t
 val get_load_paths : unit -> t list
 (** Get the current loadpath association. *)
 
-val get_paths : unit -> CUnix.physical_path list
-(** Same as [get_load_paths] but only get the physical part. *)
-
 val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
 (** [add_load_path phys log type] adds the binding [phys := log] to the current
     loadpaths. *)
@@ -52,3 +49,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
 (** As {!expand_path} but uses a filter function instead, and ignores the
     implicit status of loadpaths. *)
+
+val locate_file : string -> string
+(** Locate a file among the registered paths. Do not use this function, as
+    it does not respect the visibility of paths. *)
diff --git a/library/states.ml b/library/states.ml
index 96a487b16..3cb6da12e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,18 +21,12 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let (extern_state,intern_state) =
-  let ensure_suffix f = CUnix.make_suffix f ".coq" in
-  let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number in
-  (fun s ->
-    let s = ensure_suffix s in
-    raw_extern s (freeze ~marshallable:`Yes)),
-  (fun s ->
-    let s = ensure_suffix s in
-    let paths = Loadpath.get_paths () in
-    unfreeze (with_magic_number_check (raw_intern paths) s);
-    Library.overwrite_library_filenames s)
+let extern_state s =
+  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+
+let intern_state s =
+  unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+  Library.overwrite_library_filenames s
 
 (* Rollback. *)
 
diff --git a/man/coqide.1 b/man/coqide.1
index cfd9c3b4a..6a3e67ad5 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -63,9 +63,11 @@ Load Coq file
 (Load Verbose
 .IR f .).
 .TP
-.BI \-load\-vernac\-object\  f
-Load Coq object file
-.IR f .vo.
+.BI \-load\-vernac\-object\  path
+Load Coq library
+.IR path
+(Require
+.IR path .).
 .TP
 .BI \-require\  path
 Load Coq library
diff --git a/man/coqtop.1 b/man/coqtop.1
index e079bee39..62d17aa67 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -73,9 +73,10 @@ load verbosely Coq file
 (Load Verbose filename.)
 
 .TP
-.BI \-load\-vernac\-object \ filename
-load Coq object file
-.I filename.vo
+.BI \-load\-vernac\-object \ path
+load Coq library
+.I path
+(Require path.)
 
 .TP
 .BI \-require \ path
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6684b0604..5ae989b78 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -752,7 +752,7 @@ let define_evar_as_product evd (evk,args) =
 let define_pure_evar_as_lambda env evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = whd_betadeltaiota env evd (evar_concl evi) in
+  let typ = whd_betadeltaiota evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fae8716d9..b88913dec 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Pp.msg_notice (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
     in
     (p,status)
   with
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 4df9603dc..06bf955c8 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -104,9 +104,7 @@ let schedule_vio_compilation j fs =
     let f =
       if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
-    let paths = Loadpath.get_paths () in
-    let _, long_f_dot_v =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+    let long_f_dot_v = Loadpath.locate_file (f^".v") in
     let aux = Aux_file.load_aux_file_for long_f_dot_v in
     let eta =
       try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
diff --git a/test-suite/bugs/closed/4347.v b/test-suite/bugs/closed/4347.v
new file mode 100644
index 000000000..29686a26c
--- /dev/null
+++ b/test-suite/bugs/closed/4347.v
@@ -0,0 +1,17 @@
+Fixpoint demo_recursion(n:nat) := match n with
+                                    |0 => Type
+                                    |S k => (demo_recursion k) -> Type
+                                    end.
+
+Record Demonstration := mkDemo
+{
+    demo_law : forall n:nat, demo_recursion n;
+    demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type :=
+     match n with
+     | 0 => Type
+     | S k => demo_recursion k -> Type
+     end) n, (demo_law (S n)) q
+}.
+
+Theorem DemoError : Demonstration.
+Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*)
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
new file mode 100644
index 000000000..83016976e
--- /dev/null
+++ b/theories/Compat/Coq84.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.4 *)
+(** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
+(** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
+Require Coq.omega.Omega.
+Ltac omega := Coq.omega.Omega.omega.
+
+(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
+Global Set Asymmetric Patterns.
+
+(** See bug 3545 *)
+Global Set Universal Lemma Under Conjunction.
+
+(** In 8.4, [admit] created a new axiom; in 8.5, it just shelves the goal. *)
+Axiom proof_admitted : False.
+Ltac admit := clear; abstract case proof_admitted.
+
+(** In 8.5, [refine] leaves over dependent subgoals. *)
+Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable.
+
+(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
+Ltac constructor_84 := constructor.
+Ltac constructor_84_n n := constructor n.
+Ltac constructor_84_tac tac := once (constructor; tac).
+
+Tactic Notation "constructor" := constructor_84.
+Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
+Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
+
+Global Set Regular Subst Tactic.
+
+(** Some names have changed in the standard library, so we add aliases. *)
+Require Coq.ZArith.Int.
+Module Export Coq.
+  Module Export ZArith.
+    Module Int.
+      Module Z_as_Int.
+        Include Coq.ZArith.Int.Z_as_Int.
+        (* FIXME: Should these get a (compat "8.4")?  Or be moved to Z_as_Int, probably? *)
+        Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing).
+        Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing).
+        Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing).
+      End Z_as_Int.
+    End Int.
+  End ZArith.
+End Coq.
+
+(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
+Require Coq.Numbers.Natural.Peano.NPeano.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
new file mode 100644
index 000000000..1622f2aed
--- /dev/null
+++ b/theories/Compat/Coq85.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.5 *)
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
new file mode 100644
index 000000000..c0c40ab1c
--- /dev/null
+++ b/theories/Compat/vo.itarget
@@ -0,0 +1,2 @@
+Coq84.vo
+Coq85.vo
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 4519070e4..b7de41641 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -1,6 +1,7 @@
 Arith/vo.otarget
 Bool/vo.otarget
 Classes/vo.otarget
+Compat/vo.otarget
 FSets/vo.otarget
 MSets/vo.otarget
 MMaps/vo.otarget
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2554ed495..22febd6a6 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -61,8 +61,8 @@ let usage () =
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  -Q <dir> <coqdir>    map physical dir to Coq dir";
-  prerr_endline "  --latin1             set ISO-8859-1 input language";
-  prerr_endline "  --utf8               set UTF-8 input language";
+  prerr_endline "  --latin1             set ISO-8859-1 mode";
+  prerr_endline "  --utf8               set UTF-8 mode";
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45a..8589f94a0 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -197,8 +197,11 @@ module Latex = struct
     printf "\n";
     printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
     printf "%%interpret utf8 characters but extra packages might have to be added\n";
-    printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
-    printf "%%Use coqdoc's option -p to add new packages.\n";
+    printf "%%such as \"textgreek\" for Greek letters not already in tipa\n";
+    printf "%%or \"stmaryrd\" for mathematical symbols.\n";
+    printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n";
+    printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n";
+    printf "%%Use coqdoc's option -p to add new packages or declarations.\n";
     printf "\\usepackage{tipa}\n";
     printf "\n"
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4010806a7..076db5e11 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -144,13 +144,19 @@ let inputstate = ref ""
 let set_inputstate s =
   let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
-let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
+let inputstate () =
+  if not (String.is_empty !inputstate) then
+    let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
+    intern_state fname
 
 let outputstate = ref ""
 let set_outputstate s =
   let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
-let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
+let outputstate () =
+  if not (String.is_empty !outputstate) then
+    let fname = CUnix.make_suffix !outputstate ".coq" in
+    extern_state fname
 
 let set_include d p implicit =
   let p = dirpath_of_string p in
@@ -162,6 +168,7 @@ let add_load_vernacular verb s =
 let load_vernacular () =
   List.iter
     (fun (s,b) ->
+      let s = Loadpath.locate_file s in
       if Flags.do_beautify () then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
@@ -171,8 +178,8 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () =
-  List.iter (fun f -> Library.require_library_from_file f None)
-    (List.rev !load_vernacular_obj)
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
 
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 14d2bcea4..a0cd618e9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -97,10 +97,7 @@ let user_error loc s = Errors.user_err_loc (loc,"_",str s)
    Note: we could use only one thanks to seek_in, but seeking on and on in
    the file we parse seems a bit risky to me.  B.B.  *)
 
-let open_file_twice_if verbosely fname =
-  let paths = Loadpath.get_paths () in
-  let _,longfname =
-    find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
@@ -206,19 +203,17 @@ let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+        let fname = CUnix.make_suffix fname ".v" in
+        let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
 	if !Flags.beautify_file then
 	  begin
-            let paths = Loadpath.get_paths () in
-            let _,f = find_file_in_path ~warn:(Flags.is_verbose())
-	      paths
-	      (CUnix.make_suffix fname ".v") in
 	    chan_beautify := open_out (f^beautify_suffix);
 	    Pp.comments := []
           end;
 	begin
 	  try
-            read_vernac_file verbosely (CUnix.make_suffix fname ".v");
+            read_vernac_file verbosely f;
 	    restore_translator_coqdoc st;
 	  with reraise ->
             let reraise = Errors.push reraise in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8efcccaaa..8ae6ac2bc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -365,8 +365,7 @@ let dump_universes sorted s =
 (* "Locate" commands *)
 
 let locate_file f =
-  let paths = Loadpath.get_paths () in
-  let _, file = System.find_file_in_path ~warn:false paths f in
+  let file = Flags.silently Loadpath.locate_file f in
   str file
 
 let msg_found_library = function
@@ -930,10 +929,12 @@ let vernac_chdir = function
 
 let vernac_write_state file =
   Pfedit.delete_all_proofs ();
+  let file = CUnix.make_suffix file ".coq" in
   States.extern_state file
 
 let vernac_restore_state file =
   Pfedit.delete_all_proofs ();
+  let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
   States.intern_state file
 
 (************)
@@ -1845,9 +1846,7 @@ let vernac_load interp fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
   let input =
-    let paths = Loadpath.get_paths () in
-    let _,longfname =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+    let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
     Pcoq.Gram.parsable (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done