aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f71719cb9..a7742d866 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -700,7 +700,7 @@ let read_sec_context r =
let dir =
try Nametab.locate_section qid
with Not_found ->
- user_err_loc (loc,"read_sec_context", str "Unknown section.") in
+ user_err ~loc "read_sec_context" (str "Unknown section.") in
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest