Merge branch 'v8.5'

7 files changed, 35 insertions, 18 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index a0892bed9a..accba3121b 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
+  let () =
+    if not allow_uncaught && not (Errors.handled (fst e)) then
+      let (e, info) = e in
+      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
+      let err = Errors.make_anomaly msg in
+      Util.iraise (err, info)
+  in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 100b3772cc..729686f32d 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7cf0477f9f..1b396d57ba 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1064,7 +1064,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    let ctx = Evd.evar_universe_context_set ctx in
+    let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
     let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
@@ -1097,7 +1097,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    let ctx = Evd.evar_universe_context_set ctx in
+    let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) 
 	      fixnames fixdecls fixtypes fiximps);
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 56b5442922..934e73aae9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -58,7 +58,10 @@ let init_color () =
   | `ON -> true
   | `AUTO ->
     Terminal.has_style Unix.stdout &&
-    Terminal.has_style Unix.stderr
+    Terminal.has_style Unix.stderr &&
+    (* emacs compilation buffer does not support colors by default,
+       its TERM variable is set to "dumb". *)
+    Unix.getenv "TERM" <> "dumb"
   in
   if has_color then begin
     let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
@@ -496,6 +499,7 @@ let parse_args arglist =
     |"-async-proofs-never-reopen-branch" ->
         Flags.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
+    |"-test-mode" -> test_mode := true
     |"-beautify" -> make_beautify true
     |"-boot" -> boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
@@ -615,7 +619,8 @@ let init arglist =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any))
+      let is_anomaly e = Errors.is_anomaly e || not (Errors.handled e) in
+      fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any))
   end;
   if !batch_mode then begin
     flush_all();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 50fb019f47..36ecc9fa5f 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -58,7 +58,7 @@ let print_usage_channel co command =
 \n\
 \n  -quiet                 unset display of extra information (implies -w none)\
 \n  -w (all|none)          configure display of warnings\
-\n  -color (on|off|auto)   configure color output (only active through coqtop)\
+\n  -color (on|off|auto)   configure color output\
 \n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5418c60e94..7d84ecf6ca 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -215,7 +215,7 @@ let display_cmd_header loc com =
 	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com verbosely checknav (loc,com) =
+let rec vernac_com checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -241,7 +241,7 @@ let rec vernac_com verbosely checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp verbosely (loc,v)
+    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
@@ -268,7 +268,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com verbosely checknav loc_ast;
+      vernac_com checknav loc_ast;
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
@@ -277,6 +277,7 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
+          cur_file := None;
           if do_beautify () then
             pr_new_syntax (Loc.make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname (disable_drop e, info)
@@ -292,14 +293,14 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+let eval_expr loc_ast = vernac_com checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
-    read_vernac_file verb file;
+    Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with any ->
     let (e, info) = Errors.push any in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9d5edc80a0..188d2d098f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1563,7 +1563,7 @@ let vernac_global_check c =
   let sigma = Evd.from_env env in
   let c,ctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
-  let cstrs = snd (Evd.evar_universe_context_set ctx) in
+  let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in
   let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
@@ -1628,9 +1628,13 @@ let vernac_print = function
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
   | PrintUniverses (b, None) ->
-    let univ = Global.universes () in
-    let univ = if b then Univ.sort_universes univ else univ in
-    msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ)
+     let univ = Global.universes () in
+     let univ = if b then Univ.sort_universes univ else univ in
+     let pr_remaining =
+       if Global.is_joined_environment () then mt ()
+       else str"There may remain asynchronous universe constraints"
+     in
+     msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
   | PrintUniverses (b, Some s) -> dump_universes b s
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
@@ -2106,7 +2110,7 @@ let with_fail b f =
            | e ->
               let e = Errors.push e in
               raise (HasFailed (Errors.iprint
-                (Cerrors.process_vernac_interp_error ~with_header:false e))))
+                (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in
@@ -2114,7 +2118,7 @@ let with_fail b f =
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if is_verbose () || !Flags.ide_slave then msg_info
+          if is_verbose () || !test_mode || !ide_slave then msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end