From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 19 Aug 2016 02:35:47 +0200
Subject: Make the user_err header an optional parameter.

Suggested by @ppedrot
---
 library/nametab.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/nametab.ml')

diff --git a/library/nametab.ml b/library/nametab.ml
index 989dcf3f3..b76048e89 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -453,7 +453,7 @@ let global r =
   try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ~loc "global"
+        user_err ~loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
            pr_qualid qid)
   with Not_found ->
@@ -532,7 +532,7 @@ let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
-      user_err ~loc:(loc_of_reference r) "global_inductive"
+      user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive"
         (pr_reference r ++ spc () ++ str "is not an inductive type")
 
 
-- 
cgit v1.2.3