diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 41 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 |
2 files changed, 35 insertions, 8 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2bab04e90..be75dc9d5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1053,21 +1053,31 @@ dependencies. This tactic is the inverse of {\tt intro}. \label{move} This moves the hypothesis named {\ident$_1$} in the local context -after the hypothesis named {\ident$_2$}. The proof term is not changed. +after the hypothesis named {\ident$_2$}, where ``after'' is in +reference to the direction of the move. The proof term is not changed. -If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies, -then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) depend on {\ident$_1$} are moved too. +If {\ident$_1$} comes before {\ident$_2$} in the order of +dependencies, then all the hypotheses between {\ident$_1$} and +{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are +moved too, and all of them are thus moved after {\ident$_2$} in the +order of dependencies. If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies, then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) occur in {\ident$_1$} are moved too. +(possibly indirectly) occur in the type of {\ident$_1$} are moved +too, and all of them are thus moved before {\ident$_2$} in the order +of dependencies. \begin{Variants} \item {\tt move {\ident$_1$} before {\ident$_2$}} -This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}. +This moves {\ident$_1$} towards and just before the hypothesis named +{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}}, +dependencies over {\ident$_1$} (when {\ident$_1$} comes before +{\ident$_2$} in the order of dependencies) or in the type of +{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order +of dependencies) are moved too. \item {\tt move {\ident} at top} @@ -1084,13 +1094,30 @@ This moves {\ident} at the bottom of the local context (at the end of the contex \item \errindex{No such hypothesis} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: - it occurs in {\ident$_2$}} + it occurs in the type of {\ident$_2$}} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: it depends on {\ident$_2$}} \end{ErrMsgs} +\Example + +\begin{coq_example} +Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. +intros x H z y H0. +move x after H0. +Undo. +move x before H0. +Undo. +move H0 after H. +Undo. +move H0 before H. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + \subsection{\tt rename {\ident$_1$} into {\ident$_2$}} \tacindex{rename} diff --git a/proofs/logic.ml b/proofs/logic.ml index c329bdf4a..6af1b2d83 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -253,7 +253,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = else user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ - str (if toleft then ": it occurs in " else ": it depends on ") + str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ pr_id hyp ++ str ".") else (d::first, middle) |