Documentation for eassert, eenough, epose proof, eset, eremember, epose.

Includes fixes and suggestions from Théo.

1 files changed, 47 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fc3fdd002..def42955f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1155,6 +1155,15 @@ Section~\ref{Occurrences_clauses}.
 
   These are the general forms that combine the previous possibilities.
 
+\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\
+      {\tt eset {\term} in {\occgoalset}}
+
+  While the different variants of \texttt{set} expect that no
+  existential variables are generated by the tactic, \texttt{eset}
+  removes this constraint. In practice, this is relevant only when
+  \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the
+  term does not occur in the goal.
+
 \item {\tt remember {\term} as {\ident}}\tacindex{remember}
 
   This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a
@@ -1170,6 +1179,15 @@ Section~\ref{Occurrences_clauses}.
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
 
+\item
+  {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\
+  {\tt eremember {\term} as {\ident} in {\occgoalset}}\\
+  {\tt eremember {\term} as {\ident} eqn:{\ident}}
+
+  While the different variants of \texttt{remember} expect that no
+  existential variables are generated by the tactic, \texttt{eremember}
+  removes this constraint.
+
 \item {\tt pose ( {\ident} := {\term} )}\tacindex{pose}
 
   This adds the local definition {\ident} := {\term} to the current
@@ -1187,6 +1205,14 @@ Section~\ref{Occurrences_clauses}.
   This behaves as {\tt pose ( {\ident} := {\term} )} but
   {\ident} is generated by {\Coq}.
 
+\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\
+      {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\
+      {\tt epose {\term}}
+
+  While the different variants of \texttt{pose} expect that no
+  existential variables are generated by the tactic, \texttt{epose}
+  removes this constraint.
+
 \end{Variants}
 
 \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term}
@@ -1284,6 +1310,14 @@ in the list of subgoals remaining to prove.
 
   \ErrMsg \errindex{Variable {\ident} is already declared}
 
+\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\
+  {\tt assert ( {\ident} := {\term} )}
+
+  While the different variants of \texttt{assert} expect that no
+  existential variables are generated by the tactic, \texttt{eassert}
+  removes this constraint. This allows not to specify the asserted
+  statement completely before starting to prove it.
+
 \item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by
@@ -1294,6 +1328,11 @@ in the list of subgoals remaining to prove.
     as {\intropattern}} is the same as applying
   the {\intropattern} to {\term}.
 
+\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}}
+
+  While \texttt{pose proof} expects that no existential variables are generated by the tactic,
+  \texttt{epose proof} removes this constraint.
+
 \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
 
   This adds a new hypothesis of name {\ident} asserting {\form} to the
@@ -1320,6 +1359,14 @@ in the list of subgoals remaining to prove.
   destructed. If the \texttt{as} {\intropattern} clause generates more
   than one subgoal, {\tac} is applied to all of them.
 
+\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\
+ \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\
+ \texttt{eenough {\form} as {\intropattern} by {\tac}}
+
+  While the different variants of \texttt{enough} expect that no
+  existential variables are generated by the tactic, \texttt{eenough}
+  removes this constraint.
+
 \item {\tt cut {\form}}\tacindex{cut}
 
   This tactic applies to any goal. It implements the non-dependent