diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
index 96def3200..9d5e76dda 100644
--- a/engine/backends/coq/ssprove/ssprove_backend.ml
+++ b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -15,6 +15,7 @@ include
       include On.Mutable_variable
       include On.Loop
       include On.For_loop
+      include On.While_loop
       include On.For_index_loop
       include On.State_passing_loop
     end)
@@ -52,8 +53,10 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
+
         include Features.SUBTYPE.On.Loop
         include Features.SUBTYPE.On.For_loop
+        include Features.SUBTYPE.On.While_loop
         include Features.SUBTYPE.On.For_index_loop
         include Features.SUBTYPE.On.State_passing_loop
       end)