diff --git a/src/libraries/qed/listmap.ml b/src/libraries/qed/listmap.ml
index 0bdaa8c417858fd5438dee5c4faa22bf8f09553d..fd25962e3165fbb4a158e981a2466c3bf1e439cf 100644
--- a/src/libraries/qed/listmap.ml
+++ b/src/libraries/qed/listmap.ml
@@ -95,7 +95,10 @@ struct
       | [] -> (match f k v None with None -> l | Some w -> l @ [k,w])
       | ((k',v') as a)::next->
         let c = K.compare k k' in
-        if c < 0 then l
+        if c < 0 then
+          match f k v None with
+          | None -> l
+          | Some w -> append_until a l ((k, w) :: next)
         else if c = 0 then
           match f k v (Some v') with
           | None -> append_until a l next