Merge branch 'v8.6'

3 files changed, 15 insertions, 6 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 48a8305bc2..dbebe6a48f 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
+(* XXX: To move to common tagging functions in Pp, blocked on tag
+ * system cleanup as we cannot define generic error tags now.
+ *
+ * Anyways, tagging should not happen here, but in the specific
+ * listener to the msg_* stuff.
+ *)
+let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let err_str       = tag_err_str "Error:"
+let ann_str       = tag_err_str "Anomaly:"
+
 let _ =
   let pr = function
   | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
@@ -92,7 +102,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
            strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
            str ".")
   else
@@ -114,7 +124,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (str "Error: " ++ where s ++ pps)
+    hov 0 (err_str ++ where s ++ pps)
   | _ -> raise Unhandled
 end
 
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 500581a39e..ae25735c5f 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -22,7 +22,7 @@ let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
 let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
-let add exn ?(valid = initial) id =
+let add exn ~valid id =
   Exninfo.add exn state_id_info (valid, id)
 let get exn = Exninfo.get exn state_id_info
 
diff --git a/lib/stateid.mli b/lib/stateid.mli
index cd8fddf0ce..1d87a343b3 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -26,9 +26,8 @@ val newer_than : t -> t -> bool
 
 (* Attaches to an exception the concerned state id, plus an optional
  * state id that is a valid state id before the error.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
 val get : Exninfo.info -> (t * t) option
 
 type ('a,'b) request = {