Document [pop_many].

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}

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