aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 77837fefc..dfea25dd0 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -269,7 +269,7 @@ let universe_context ~names ~extensible ctx =
try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
with Not_found ->
user_err ?loc ~hdr:"universe_context"
- (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+ (str"Universe " ++ Id.print id ++ str" is not bound anymore.")
in (l :: newinst, Univ.LSet.remove l acc))
names ([], levels)
in