diff --git a/doc/main.tex b/doc/main.tex
index 7e1f2b586edfa898c93c87989ac046bcf85d1b54..80fe20c460e74b36a262889b696b10a6ccec16f8 100644
--- a/doc/main.tex
+++ b/doc/main.tex
@@ -2525,6 +2525,17 @@ this stack element is the current state of the automaton. If the stack is
 empty, \verb+None+ is returned. In that case, the current state of the
 automaton must be an initial state.
 
+%% val pop_many
+
+\begin{verbatim}
+  val pop_many: int -> 'a env -> 'a env option
+\end{verbatim}
+
+\verb+pop_many i env+ pops \verb+i+ elements off the automaton's stack. This
+is done via \verb+i+ successive invocations of \verb+pop+. Thus,
+\verb+pop_many 1+ is \verb+pop+. The index \verb+i+ must be nonnegative. The
+time complexity is $O(i)$.
+
 %% val positions
 
 \begin{verbatim}
diff --git a/src/IncrementalEngine.ml b/src/IncrementalEngine.ml
index cb26816e57a85b81e0f2be7e61c9630f6f4f7d32..c90319029abd8343371ea8a15173a6bccface1e1 100644
--- a/src/IncrementalEngine.ml
+++ b/src/IncrementalEngine.ml
@@ -269,8 +269,8 @@ module type INCREMENTAL_ENGINE = sig
 
   val top: 'a env -> element option
 
-  (* [pop_many i env] pops [i] cells off the automaton's stack. This is done by
-     invoking [pop] [i] times in succession. Thus, [pop_many 1] is [pop]. The
+  (* [pop_many i env] pops [i] cells off the automaton's stack. This is done
+     via [i] successive invocations of [pop]. Thus, [pop_many 1] is [pop]. The
      index [i] must be nonnegative. The time complexity is O(i). *)
 
   val pop_many: int -> 'a env -> 'a env option