Évolutions diverses et variées.

- Correction divers messages d'erreur
  - lorsque rien à réécrire dans une hyp,
  - lorsqu'une variable ltac n'est pas liée,
  - correction anomalie en présence de ?id dans le "as" de induction,
  - correction mauvais env dans message d'erreur de unify_0.

- Diverses extensions et améliorations
  - "specialize" :
    - extension au cas (fun x1 ... xn => H u1 ... un),
    - renommage au même endroit.
  - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
  - "induction"
    - intro des IH toujours au sommet même si induction sur var quantifiée,
    - ajout d'un hack pour la reconnaissance de schémas inductifs comme
      N_ind_double mais il reste du boulot pour reconnaître (et/ou
      réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
      dans l'ordre standard,
    - vérification de longueur et éventuelle complétion des
      intropatterns dans le cas de sous-patterns destructifs dans induction
      (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
       le n dans le contexte),
    - localisation des erreurs d'intropattern,
    - ajout d'un pattern optionnel après "as" pour forcer une égalité et la
      nommer (*).
  - "apply" accepte plusieurs arguments séparés par des virgules (*).
  - Plus de robustesse pour clear en présence d'evars.
  - Amélioration affichage TacFun dans Print Ltac.
  - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
    (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
  - Fusion VTactic/VFun dans l'espoir.
  - Mise en place d'un système de trace de la pile des appels Ltac (tout en
    préservant certains aspects de la récursivité terminale - cf bug #468).

- Tactiques primitives

  - ajout de "move before" dans les tactiques primitives et ajout des
    syntaxes move before et move dependent au niveau utilisateur (*),
  - internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
  - suppression de Intro_replacing et du code sous-traitant

- Nettoyage
  - Suppression cible et fichiers minicoq non portés depuis longtemps.

(*) Extensions de syntaxe qu'il pourrait être opportun de discuter



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

1 files changed, 146 insertions, 61 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9f6fa8be1..54237d721 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -174,7 +174,8 @@ usable in the proof development.
 \end{ErrMsgs}
 
 \subsection{\tt move {\ident$_1$} after {\ident$_2$}
-\tacindex{move}}
+\tacindex{move}
+\label{move}}
 
 This moves the hypothesis named {\ident$_1$} in the local context
 after the hypothesis named {\ident$_2$}.
@@ -187,6 +188,32 @@ If {\ident$_1$} comes after {\ident$_2$} in the order of dependences,
 then all hypotheses between {\ident$_1$} and {\ident$_2$} which 
 (possibly indirectly) occur in {\ident$_1$} are moved also.
 
+\begin{Variants}
+
+\item {\tt move {\ident$_1$} before {\ident$_2$}}
+
+This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}.
+
+\item {\tt move {\ident} at top}
+
+This moves {\ident} at the top of the local context (at the beginning of the context).
+
+\item {\tt move {\ident} at bottom}
+
+This moves {\ident} at the bottom of the local context (at the end of the context).
+
+\item {\tt move dependent {\ident$_1$} after {\ident$_2$}}\\
+      {\tt move dependent {\ident$_1$} before {\ident$_2$}}\\
+      {\tt move dependent {\ident$_1$} at top}\\
+      {\tt move dependent {\ident$_1$} at bottom}
+
+This moves {\ident$_1$} towards the specified place. All the
+hypotheses that recursively depend on, for a downwards move, or
+in, for an upwards move, the hypothesis {\ident$_1$} are moved
+too so as to respect the order of dependencies between hypotheses.
+
+\end{Variants}
+
 \begin{ErrMsgs}
 
 \item \errindex{{\ident$_i$} not found}
@@ -316,22 +343,32 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic
   Happens when {\num} is 0 or is greater than the number of non-dependent
   products of the goal.
 
-\item {\tt intro after \ident} \tacindex{intro after}
+\item {\tt intro after \ident} \tacindex{intro after}\\
+      {\tt intro before \ident} \tacindex{intro before}\\
+      {\tt intro at top} \tacindex{intro at top}\\
+      {\tt intro at bottom} \tacindex{intro at bottom}
 
-  Applies {\tt intro} but puts the introduced
-  hypothesis after the hypothesis \ident{} in the hypotheses.
+  Applies {\tt intro} and moves the freshly introduced hypothesis
+  respectively after the hypothesis \ident{}, before the hypothesis
+  \ident{}, at the top of the local context, or at the bottom of the
+  local context. All hypotheses on which the new hypothesis depends
+  are moved too so as to respect the order of dependencies between
+  hypotheses. Note that {\tt intro as bottom} is is a synonym for {\tt
+  intro} with no argument.
 
 \begin{ErrMsgs}
 \item \errindex{No product even after head-reduction}
 \item \errindex{No such hypothesis} : {\ident}
 \end{ErrMsgs}
 
-\item {\tt intro \ident$_1$ after \ident$_2$}
-  \tacindex{intro ... after}
+\item {\tt intro \ident$_1$ after \ident$_2$}\\
+      {\tt intro \ident$_1$ before \ident$_2$}\\
+      {\tt intro \ident$_1$ at top}\\
+      {\tt intro \ident$_1$ at bottom}
   
-  Behaves as previously but \ident$_1$ is the name of the introduced
-  hypothesis.  It is equivalent to {\tt intro \ident$_1$; move
-    \ident$_1$ after \ident$_2$}.
+  Behaves as previously but naming the introduced hypothesis
+  \ident$_1$.  It is equivalent to {\tt intro \ident$_1$} followed by
+  the appropriate call to {\tt move}~(see Section~\ref{move}).
 
 \begin{ErrMsgs}
 \item \errindex{No product even after head-reduction}
@@ -404,6 +441,14 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   premises. Here, variables are referred by names and non-dependent
   products by increasing numbers (see syntax in Section~\ref{Binding-list}).
 
+\item {\tt apply} {\term$_1$} {\tt ,} \ldots {\tt ,} {\term$_n$} 
+
+  This is a shortcut for {\tt apply} {\term$_1$} {\tt ; [ ..~|}
+   \ldots~{\tt ; [ ..~| {\tt apply} {\term$_n$} ]} \ldots~{\tt ]}, i.e. for the
+   successive applications of {\term$_{i+1}$} on the last subgoal
+   generated by {\tt apply} {\term$_i$}, starting from the application
+   of {\term$_1$}.
+
 \item {\tt eapply \term}\tacindex{eapply}\label{eapply}
   
   The tactic {\tt eapply} behaves as {\tt apply} but does not fail
@@ -417,6 +462,29 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   An example of use of {\tt eapply} is given in
   Section~\ref{eapply-example}. 
 
+\item {\tt simple apply {\term}} \tacindex{simple apply} 
+
+  This behaves like {\tt apply} but it reasons modulo conversion only
+  on subterms that contain no variables to instantiate. For instance,
+  if {\tt id := fun x:nat => x} and {\tt H : forall y, id y = y} then
+  {\tt simple apply H} on goal {\tt O = O} does not succeed because it
+  would require the conversion of {\tt f ?y} and {\tt O} where {\tt
+  ?y} is a variable to instantiate. Tactic {\tt simple apply} does not
+  either traverse tuples as {\tt apply} does.
+
+  Because it reasons modulo a limited amount of conversion, {\tt
+  simple apply} fails quicker than {\tt apply} and it is then
+  well-suited for uses in used-defined tactics that backtrack often.
+
+\item \zeroone{{\tt simple}} {\tt apply} {\term$_1$} \zeroone{{\tt with}
+  {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
+  {\bindinglist$_n$}}\\
+  \zeroone{{\tt simple}} {\tt eapply} {\term$_1$} \zeroone{{\tt with}
+  {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
+  {\bindinglist$_n$}}
+
+  This summarizes the difference syntaxes for {\tt apply}.
+
 \item {\tt lapply {\term}} \tacindex{lapply} 
 
   This tactic applies to any goal, say {\tt G}.  The argument {\term}
@@ -911,7 +979,7 @@ $\!\!\!$\begin{tabular}{lcl}
 & | &
     {\tt *}\\
 {\atoccurrences} & ::= & {\tt at} {\occlist}\\
-{\occlist} & ::= & \zeroone{\tt -} {\num$_1$} \dots\ {\num$_n$}
+{\occlist} & ::= & \zeroone{{\tt -}} {\num$_1$} \dots\ {\num$_n$}
 \end{tabular}
 
 The role of an occurrence clause is to select a set of occurrences of
@@ -1483,24 +1551,35 @@ induction n.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item{\tt induction {\term} as {\intropattern}}
+\item{\tt induction {\term} as {\disjconjintropattern}}
   
   This behaves as {\tt induction {\term}} but uses the names in
-  {\intropattern} to name the variables introduced in the context.
-  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
+  {\disjconjintropattern} to name the variables introduced in the context.
+  The {\disjconjintropattern} must typically be of the form
+  {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
     ]} with $m$ being the number of constructors of the type of
   {\term}. Each variable introduced by {\tt induction} in the context
   of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt induction}
   invents names for the remaining variables to introduce. More
-  generally, the $p_{ij}$ can be any introduction patterns (see
-  Section~\ref{intros-pattern}). This provides a concise notation for
-  nested induction.
+  generally, the $p_{ij}$ can be any disjunctive/conjunctive
+  introduction pattern (see Section~\ref{intros-pattern}). For instance,
+  for an inductive type with one constructor, the pattern notation
+  {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
+  {\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
+
+\item{\tt induction {\term} as {\namingintropattern}}
+
+  This behaves as {\tt induction {\term}} but adds an equation between
+  {\term} and the value that {\term} takes in each of the induction
+  case.  The name of the equation is built according to
+  {\namingintropattern} which can be an identifier, a ``?'', etc, as
+  indicated in Section~\ref{intros-pattern}.
 
-\Rem for an inductive type with one constructor, the pattern notation
-{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
-{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
+\item{\tt induction {\term} as {\namingintropattern} {\disjconjintropattern}}
+
+  This combines the two previous forms.
 
 \item{\tt induction {\term} with \bindinglist}
 
@@ -1533,11 +1612,6 @@ induction n.
   with complex predicates as the induction principles generated by
   {\tt Function} or {\tt Functional Scheme} may be.
 
-\item \texttt{induction {\term} in *}
-
-  This syntax tells to keep an equation between {\term} and the value
-  it gets in each case of the induction.
-
 \item \texttt{induction {\term} in {\occgoalset}}
 
   This syntax is used for selecting which occurrences of {\term} the
@@ -1547,12 +1621,13 @@ induction n.
 
   When an occurrence clause is given, an equation between {\term} and
   the value it gets in each case of the induction is added to the
-  context of the subgoals corresponding to the induction cases.
+  context of the subgoals corresponding to the induction cases (even
+  if no clause {\tt as {\namingintropattern}} is given.
 
-\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
-  This is the most general form of {\tt induction} and {\tt
+  These are the most general forms of {\tt induction} and {\tt
   einduction}.  It combines the effects of the {\tt with}, {\tt as},
   {\tt using}, and {\tt in} clauses.
 
@@ -1598,7 +1673,7 @@ instantiate premises of the type of {\term$_2$}.
 \item{\tt elim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}\\
      {\tt eelim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}
 
-  This is the most general form of {\tt elim} and {\tt eelim}.  It
+  These are the most general forms of {\tt elim} and {\tt eelim}.  It
   combines the effects of the {\tt using} clause and of the two uses
   of the {\tt with} clause.
 
@@ -1663,7 +1738,7 @@ last introduced hypothesis.
 \end{itemize}
 
 \begin{Variants}
-\item{\tt destruct {\term} as {\intropattern}}
+\item{\tt destruct {\term} as {\disjconjintropattern}}
   
   This behaves as {\tt destruct {\term}} but uses the names in
   {\intropattern} to name the variables introduced in the context.
@@ -1674,16 +1749,24 @@ last introduced hypothesis.
   of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
   invents names for the remaining variables to introduce. More
-  generally, the $p_{ij}$ can be any introduction patterns (see
-  Section~\ref{intros-pattern}). This provides a concise notation for
-  nested destruction.
+  generally, the $p_{ij}$ can be any disjunctive/conjunctive
+  introduction pattern (see Section~\ref{intros-pattern}). This
+  provides a concise notation for nested destruction.
 
 %  It is recommended to use this variant of {\tt destruct} for 
 %  robust proof scripts.
 
-\Rem for an inductive type with one constructor, the pattern notation
-{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
-{\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
+\item{\tt destruct {\term} as {\namingintropattern}}
+
+  This behaves as {\tt destruct {\term}} but adds an equation between
+  {\term} and the value that {\term} takes in each of the possible
+  cases.  The name of the equation is built according to
+  {\namingintropattern} which can be an identifier, a ``?'', etc, as
+  indicated in Section~\ref{intros-pattern}.
+
+\item{\tt destruct {\term} as {\namingintropattern} {\disjconjintropattern}}
+
+  This combines the two previous forms.
 
 \item{\tt destruct {\term} with \bindinglist}
 
@@ -1709,11 +1792,6 @@ last introduced hypothesis.
   These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and
   {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}.
 
-\item \texttt{destruct {\term} in *}
-
-  This syntax tells to keep an equation between {\term} and the value
-  it gets in each cases of the analysis.
-
 \item \texttt{destruct {\term} in {\occgoalset}}
 
   This syntax is used for selecting which occurrences of {\term} the
@@ -1723,12 +1801,13 @@ last introduced hypothesis.
 
   When an occurrence clause is given, an equation between {\term} and
   the value it gets in each cases of the analysis is added to the
-  context of the subgoals corresponding to the cases.
+  context of the subgoals corresponding to the cases (even
+  if no clause {\tt as {\namingintropattern}} is given.
 
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
-  This is the most general form of {\tt destruct} and {\tt edestruct}.
+  These are the general forms of {\tt destruct} and {\tt edestruct}.
   It combines the effects of the {\tt with}, {\tt as}, {\tt using},
   and {\tt in} clauses.
 
@@ -1781,18 +1860,24 @@ last introduced hypothesis.
 \tacindex{intros \intropattern}}
 
 This extension of the tactic {\tt intros} combines introduction of
-variables or hypotheses and case analysis. An introduction pattern is
+variables or hypotheses and case analysis. An {\em introduction pattern} is
 either:
 \begin{itemize}
-\item the wildcard: {\tt \_}
-\item the pattern \texttt{?}
-\item the pattern \texttt{?\ident}
-\item an identifier
-\item a disjunction of lists of patterns:
+\item A {\em naming introduction pattern}, i.e. either one of:
+  \begin{itemize}
+  \item the pattern \texttt{?}
+  \item the pattern \texttt{?\ident}
+  \item an identifier
+  \end{itemize}
+\item A {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
+  \begin{itemize}
+  \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
-\item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
-\item a list of patterns {\tt (} $p_1$\ {\tt \&}\ {\ldots}\ {\tt \&}\ $p_n$ {\tt )}
- for sequence of right-associative binary constructs
+  \item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
+  \item a list of patterns {\tt (} $p_1$\ {\tt \&}\ {\ldots}\ {\tt \&}\ $p_n$ {\tt )}
+   for sequence of right-associative binary constructs
+  \end{itemize}
+\item the wildcard: {\tt \_}
 \item the rewriting orientations: {\tt ->} or {\tt <-}
 \end{itemize}
 
@@ -1801,13 +1886,6 @@ of type {\tt forall $x$:$T$, $P$} (dependent product), the behavior of
 {\tt intros $p$} is defined inductively over the structure of the
 introduction pattern $p$:
 \begin{itemize}
-\item introduction on the wildcard depends on whether the product is
-  dependent or not: in the non dependent case, it erases the
-  corresponding hypothesis (i.e. it behaves as an {\tt intro} followed
-  by a {\tt clear}, cf Section~\ref{clear}) while in the dependent
-  case, it succeeds and erases the variable only if the wildcard is
-  part of a more complex list of introduction patterns that also
-  erases the hypotheses depending on this variable;
 \item introduction on \texttt{?} performs the introduction, and let {\Coq}
   choose a fresh name for the variable;
 \item introduction on \texttt{?\ident} performs the introduction, and
@@ -1843,6 +1921,13 @@ introduction pattern $p$:
   constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
   hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
   introduced via pattern {\tt (a \& x \& b \& c \& d)};
+\item introduction on the wildcard depends on whether the product is
+  dependent or not: in the non dependent case, it erases the
+  corresponding hypothesis (i.e. it behaves as an {\tt intro} followed
+  by a {\tt clear}, cf Section~\ref{clear}) while in the dependent
+  case, it succeeds and erases the variable only if the wildcard is
+  part of a more complex list of introduction patterns that also
+  erases the hypotheses depending on this variable;
 \item introduction over {\tt ->} (respectively {\tt <-}) expects the
   hypothesis to be an equality and the right-hand-side (respectively
   the left-hand-side) is replaced by the left-hand-side (respectively