aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r--kernel/uGraph.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6971c0a2b..487257a77 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -132,7 +132,7 @@ let rec repr g u =
let a =
try UMap.find u g.entries
with Not_found -> CErrors.anomaly ~label:"Univ.repr"
- (str"Universe " ++ Level.pr u ++ str" undefined")
+ (str"Universe " ++ Level.pr u ++ str" undefined.")
in
match a with
| Equiv v -> repr g v