Adding a syntax "enough" for the variant of "assert" with the order of

subgoals and the role of the "by tac" clause swapped.

1 files changed, 43 insertions, 16 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9bba45bea..28d854eaa 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1179,22 +1179,6 @@ in the list of subgoals remaining to prove.
   This behaves as {\tt assert ( {\ident} :\ {\form} )} but
   {\ident} is generated by {\Coq}.
 
-\item{\tt assert ( {\ident} := {\term} )}
-
-  This behaves as {\tt assert ({\ident} :\ {\type});[exact
-    {\term}|idtac]} where {\type} is the type of {\term}.
-
-  \ErrMsg \errindex{Variable {\ident} is already declared}
-
-\item {\tt cut {\form}}\tacindex{cut}
-
-  This tactic applies to any goal. It implements the non-dependent
-  case of the ``App''\index{Typing rules!App} rule given in
-  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
-  {\tt cut U} transforms the current goal \texttt{T} into the two
-  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
-    -> T} comes first in the list of remaining subgoal to prove.
-
 \item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
 
   This tactic behaves like \texttt{assert} but applies {\tac}
@@ -1217,6 +1201,14 @@ in the list of subgoals remaining to prove.
 
   This combines the two previous variants of {\tt assert}.
 
+\item{\tt assert ( {\ident} := {\term} )}
+
+  This behaves as {\tt assert ({\ident} :\ {\type});[exact
+      {\term}|idtac]} where {\type} is the type of {\term}. This is
+  deprecated in favor of {\tt pose proof}.
+
+  \ErrMsg \errindex{Variable {\ident} is already declared}
+
 \item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert T as {\intropattern} by
@@ -1227,6 +1219,41 @@ in the list of subgoals remaining to prove.
   {\disjconjintropattern}\tacindex{pose proof}} behaves
   like \texttt{destruct {\term} as {\disjconjintropattern}}.
 
+\item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
+
+  This adds a new hypothesis of name {\ident} asserting {\form} to the
+  goal the tactic \texttt{enough} is applied to. A new subgoal stating
+  \texttt{\form} is inserted after the initial goal rather than before
+  it as \texttt{assert} would do.
+
+\item \texttt{enough {\form}}\tacindex{enough}
+
+  This behaves like \texttt{enough ({\ident} :\ {\form})} with the name
+  {\ident} of the hypothesis generated by {\Coq}.
+
+\item \texttt{enough {\form} as {\intropattern}\tacindex{enough as}}
+
+  This behaves like \texttt{enough} {\form} using {\intropattern} to
+  name or destruct the new hypothesis.
+
+\item \texttt{enough ({\ident} :\ {\form}) by {\tac}}\tacindex{enough by}\\
+ \texttt{enough {\form} by {\tac}}\tacindex{enough by}\\
+ \texttt{enough {\form} as {\intropattern} by {\tac}}
+
+  This behaves as above but with {\tac} expected to solve the initial
+  goal after the extra assumption {\form} is added and possibly
+  destructed. If the \texttt{as} {\intropattern} clause generates more
+  than one subgoal, {\tac} is applied to all of them.
+
+\item {\tt cut {\form}}\tacindex{cut}
+
+  This tactic applies to any goal. It implements the non-dependent
+  case of the ``App''\index{Typing rules!App} rule given in
+  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
+  {\tt cut U} transforms the current goal \texttt{T} into the two
+  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
+    -> T} comes first in the list of remaining subgoal to prove.
+
 \item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\
       {\tt specialize {\ident} with \bindinglist}