A tactic shelve_unifiable.

Puts on the shelf every goals under focus on which other goals under focus
depend. Useful when we want to solve these goals by unification (as in a
first order proof search procedure, for instance).

Also meant to be able to recover approximately the semantics of the old
refine with the new implementation (use refine t; shelve_unifiable).

TODO: bug dans l'example de shelve_unifiable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 81e7db6dc0..a78e3448ea 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4621,6 +4621,26 @@ This tactic moves all goals under focus to a shelf. While on the shelf, goals
 will not be focused on. They can be solved by unification, or they can be called
 back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 
+\begin{Variants}
+  \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable}
+
+    Shelves only these goals under focused which are mentioned in other goals.
+    Goals which appear in the type of other goals can be solve by unification.
+    
+\Example
+\begin{coq_example}
+Goal exists n, n=0.
+refine (ex_intro _ _ _).
+all:shelve_unifiable.
+reflexivity.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\end{Variants}
+
 \subsection[\tt Unshelve]{\tt Unshelve\comindex{Unshelve}\label{unshelve}}
 
 This command moves all the goals on the shelf (see Section~\ref{shelve}) from the