Merge pull request PrincetonUniversity#659 from PrincetonUniversity/e…

…ntailer

Add rep_lia to Catalog; closes PrincetonUniversity#628

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.