Merge branch 'master' into econstr

5 files changed, 22 insertions, 23 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 0393669d4..781bf3223 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -143,7 +143,7 @@ let interp_definition pl bl p red_option c ctypopt =
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
 
 let check_definition (ce, evd, _, imps) =
-  check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
+  check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
 let warn_local_declaration =
@@ -305,7 +305,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
       ((env,ienv),((is_coe,idl),t,imps))) 
     (env,empty_internalization_env) l
   in
-  let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
+  let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
   (* The universe constraints come from the whole telescope. *)
   let evd = Evd.nf_constraints evd in
   let ctx = Evd.universe_context_set evd in
@@ -614,7 +614,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
      () in
 
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in
+  let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in
   evdref := sigma;
   (* Compute renewed arities *)
   let nf,_ = e_nf_evars_and_universes evdref in
@@ -1174,7 +1174,7 @@ let interp_recursive isfix fixl notations =
   (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
-  check_evars_are_solved env evd (Evd.empty,evd);
+  check_evars_are_solved env evd Evd.empty;
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env evd isfix (List.combine fixnames fixdefs)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f5d7a661e..993a2c260 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     let flags = all_and_fail_flags in
     let flags = { flags with use_hook = inference_hook } in
-    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
+    evdref := solve_remaining_evars flags env !evdref Evd.empty;
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
diff --git a/vernac/record.ml b/vernac/record.ml
index 490a2a49d..8b4b7606f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -145,7 +145,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
   let sigma = 
-    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
+    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
   let evars, nf = Evarutil.nf_evars_and_universes sigma in
   let arity = nf t' in
   let arity, evars = 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f843484f7..ee5536692 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -108,7 +108,7 @@ end
 
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
-let msgnl_with fmt strm =
+let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
 
@@ -136,20 +136,19 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
+let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
-let make_body quoter info ?loc s =
-  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  quoter (hov 0 (loc ++ info ++ s))
+let make_body quoter info ?pre_hdr s =
+  pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
-let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?loc msg)
-  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
-  (* XXX: What to do with loc here? *)
-  | Notice  -> msgnl_with !std_ft msg
+let gen_logger dbg err ?pre_hdr level msg = match level with
+  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?pre_hdr msg)
+  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
+  | Notice  -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?loc msg)
+               msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?pre_hdr msg)
 
 (** Standard loggers *)
 
@@ -158,8 +157,8 @@ let gen_logger dbg err ?loc level msg = match level with
 *)
 let std_logger_cleanup = ref (fun () -> ())
 
-let std_logger ?loc level msg =
-  gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
+let std_logger ?pre_hdr level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?pre_hdr level msg;
   !std_logger_cleanup ()
 
 (** Color logging. Moved from Ppstyle, it may need some more refactoring  *)
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 1555f80a9..909dd7077 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -38,11 +38,11 @@ val get_margin : unit -> int option
 
 (** Headers for tagging *)
 val err_hdr : Pp.std_ppcmds
+val ann_hdr : Pp.std_ppcmds
 
-(** Console display of feedback *)
-val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
-
-val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+(** Console display of feedback, we may add some location information *)
+val std_logger   : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
+val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
 
 val init_color_output : unit -> unit
 val clear_styles : unit -> unit