Merge remote-tracking branch 'upstream/trunk' into trunk

5 files changed, 18 insertions, 13 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 16fe405551..f36d0c348e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -126,14 +126,12 @@ let init_ocaml_path () =
     Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir Coq_config.all_src_dirs
 
-let get_compat_version = function
+let get_compat_version ?(allow_old = true) = function
   | "8.7" -> Flags.Current
   | "8.6" -> Flags.V8_6
   | "8.5" -> Flags.V8_5
-  | "8.4" -> Flags.V8_4
-  | "8.3" -> Flags.V8_3
-  | "8.2" -> Flags.V8_2
-  | ("8.1" | "8.0") as s ->
+  | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+    if allow_old then Flags.VOld else
     CErrors.user_err ~hdr:"get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
   | s -> CErrors.user_err ~hdr:"get_compat_version"
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 3b42289eec..787dfb61a9 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -25,4 +25,4 @@ val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
 
-val get_compat_version : string -> Flags.compat_version
+val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 908786565e..0b0ef67176 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -187,7 +187,7 @@ end
     from cycling. *)
 let make_prompt () =
   try
-    (Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < "
+    (Names.Id.to_string (Proof_global.get_current_proof_name ())) ^ " < "
   with Proof_global.NoCurrentProof ->
     "Coq < "
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 31450ebd51..5f0716fd9f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -205,9 +205,9 @@ let require () =
 
 let add_compat_require v =
   match v with
-  | Flags.V8_4 -> add_require "Coq.Compat.Coq84"
   | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
-  | _ -> ()
+  | Flags.V8_6 -> add_require "Coq.Compat.Coq86"
+  | Flags.VOld | Flags.Current -> ()
 
 let compile_list = ref ([] : (bool * string) list)
 
@@ -514,7 +514,9 @@ let parse_args arglist =
     |"-async-proofs-delegation-threshold" ->
         Flags.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
-    |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
+    |"-compat" ->
+        let v = get_compat_version ~allow_old:false (next ()) in
+        Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a61ade7849..74c7663ca5 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -111,7 +111,7 @@ let pr_open_cur_subgoals () =
   with Proof_global.NoCurrentProof -> Pp.str ""
 
 let vernac_error msg =
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg;
+  Topfmt.std_logger Feedback.Error msg;
   flush_all ();
   exit 1
 
@@ -285,8 +285,13 @@ let ensure_exists f =
 (* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
-    let pfs = Pfedit.get_all_proof_names () in
-    if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
+    let pfs = Proof_global.get_all_proof_names () in
+    if not (List.is_empty pfs) then
+      vernac_error (str "There are pending proofs: "
+                    ++ (pfs
+                        |> List.rev
+                        |> prlist_with_sep pr_comma Names.Id.print)
+                    ++ str ".")
   in
   match !Flags.compilation_mode with
   | BuildVo ->