[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

1 files changed, 3 insertions, 3 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 35ddf2e8cf..279295a03c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -196,10 +196,10 @@ let qualid_of_global env r =
 
 let safe_gen f env sigma c =
   let orig_extern_ref = Constrextern.get_extern_reference () in
-  let extern_ref loc vars r =
-    try orig_extern_ref loc vars r
+  let extern_ref ?loc vars r =
+    try orig_extern_ref ?loc vars r
     with e when CErrors.noncritical e ->
-      Libnames.Qualid (loc, qualid_of_global env r)
+      Libnames.Qualid (Loc.tag ?loc @@ qualid_of_global env r)
   in
   Constrextern.set_extern_reference extern_ref;
   try