diff --git a/write_image/WritePPM.v b/write_image/WritePPM.v
index 1f0992ad..edb896d8 100644
--- a/write_image/WritePPM.v
+++ b/write_image/WritePPM.v
@@ -164,5 +164,5 @@ Elpi Accumulate lp:{{
     close_out OSTREAM
   .
 }}.
-Elpi Typecheck.
+