diff --git a/doc/VC.pdf b/doc/VC.pdf
index d834f7d88..4bb947d0b 100644
Binary files a/doc/VC.pdf and b/doc/VC.pdf differ
diff --git a/doc/VC.tex b/doc/VC.tex
index bbc735bb7..7f089656e 100755
--- a/doc/VC.tex
+++ b/doc/VC.tex
@@ -4967,6 +4967,10 @@ \chapter{Catalog of tactics/lemmas}
 (tactic; \autopageref{refcard:entailer}, \autopageref{refcard:entailments})
 Like \lstinline{entailer}, but faster and more powerful---however,
 it sometimes turns a provable goal into an unprovable goal.
+\item[\textsf{entailer!!}]
+(tactic; \autopageref{refcard:entailer}, \autopageref{refcard:entailments})
+  Like \lstinline{entailer!}, but does not put hypotheses above the line
+  derived from SEP and LOCAL clauses.
 
 \item[\textsf{Exists} $v$]
 (tactic; \autoref{refcard:EX})
@@ -5047,6 +5051,12 @@ \chapter{Catalog of tactics/lemmas}
 proof goal for abstracting/factoring out as a separate lemma.
 % Superordinate tactics:  $\mathit{semax\_subcommand}$\\
 
+\item[\textsf{rep\_lia}]
+  (tactic; \autopageref{refcard:rep-lia})
+  Solves goals in linear integer arithmetic (like \lstinline{lia}) enhanced
+  by extra facts about 32-bit and 64-bit modular representations of integers
+  (Int and Int64 modules).
+
 \item[\textsf{semax\_subcommand\ $V$\ $G$\ $F$}]
 (tactic)
 Applicable to a proof state with a semax goal.