diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 47 |
2 files changed, 51 insertions, 0 deletions
@@ -26,6 +26,10 @@ Tactics now uses type classes and rejects terms with unresolved holes, like entry "constr" does. To get the former behavior use "open_constr_with_bindings" (possible source of incompatibility. +- New e-variants eassert, eenough, epose proof, eset, eremember, epose + which behave like the corresponding variants with no "e" but turn + unresolved implicit arguments into existential variables, on the + shelf, rather than failing. Vernacular Commands 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 |