diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index 47b928803f3ca04678a64d59840aa9b648ee4322..fcf0c43e7637aaf33fda1f173e43ec6e8aac8d67 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -339,4 +339,4 @@ Section stype.
     - iDestruct "H" as (w ->) "[H HP]".
       wp_pures. iApply "HΦ". iFrame.
   Qed.
-End stype.
+End stype.