diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e6073d109dac4da646e25e211b3e72a5aeb41549..585a95e4e258eb9bf712a961af0e3ecd433f1987 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -9,7 +9,8 @@ Section sum.
   Context `{typeG Σ}.
 
   (* We define the actual empty type as being the empty sum, so that it is
-     convertible to it (and in particular, we can partern-match on it). *)
+     convertible to it---and in particular, we can pattern-match on it
+     (as in, pattern-match in the language of lambda-rust, not in Coq). *)
   Program Definition emp0 : type :=
     {| ty_size := 1%nat;
        ty_own tid vl := False%I;