Make the user_err header an optional parameter.

Suggested by @ppedrot

5 files changed, 11 insertions, 11 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 7d3cb7e491..0dbe082311 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -71,7 +71,7 @@ let error_level_assoc p current expected =
     | Extend.LeftA -> str "left"
     | Extend.RightA -> str "right"
     | Extend.NonA -> str "non" in
-  user_err ""
+  user_err 
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative.")
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 92a59be430..7021e52702 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -56,7 +56,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
     CErrors.user_err ~loc:aloc
-      "Constr:mk_cofixb"
+      ~hdr:"Constr:mk_cofixb"
       (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
@@ -381,12 +381,12 @@ GEXTEND Gram
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
 	  | CPatCstr (_, r, None, l2) -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) "compound_pattern"
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
               (Pp.str "Nested applications not supported.")
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
           | _ -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) "compound_pattern"
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
               (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
         CPatCstr (!@loc, r, Some lp, []) ]
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b447a5de5d..820514b08a 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -28,7 +28,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    CErrors.user_err ~loc "" (Pp.str "Cannot support a so large number.")
+    CErrors.user_err ~loc  (Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
@@ -93,7 +93,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err ~loc:(!@loc) "" (Pp.str"Empty string."); s
+        if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2cc2b01c00..3c2c45c72c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -136,7 +136,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     user_err ~loc:aloc
-      "Constr:mk_cofix_tac"
+      ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
 
@@ -192,7 +192,7 @@ let merge_occurrences loc cl = function
   | None ->
       if Locusops.clause_with_generic_occurrences cl then (None, cl)
       else
-	user_err ~loc "" (str "Found an \"at\" clause without \"with\" clause.")
+	user_err ~loc  (str "Found an \"at\" clause without \"with\" clause.")
   | Some (occs, p) ->
     let ans = match occs with
     | AllOccurrences -> cl
@@ -204,9 +204,9 @@ let merge_occurrences loc cl = function
         { cl with onhyps = Some [(occs, id), l] }
       | _ ->
         if Locusops.clause_with_generic_occurrences cl then
-          user_err ~loc "" (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+          user_err ~loc  (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
         else
-          user_err ~loc "" (str "Cannot use clause \"at\" twice.")
+          user_err ~loc  (str "Cannot use clause \"at\" twice.")
       end
     in
     (Some p, ans)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c09693b364..7cb897cf71 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -115,7 +115,7 @@ GEXTEND Gram
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
                     | _ ->
-                        VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
+                        VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end ] ]
   ;
   located_vernac: