- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


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

1 files changed, 44 insertions, 30 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9589963fe..f71d66319 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -447,10 +447,10 @@ replacement only in the conclusion.
 
 \begin{Variants}
 
-\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occset}}
+\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}}
 
 This notation allows to specify which occurrences of {\term} have to
-be substituted in the context. The {\tt in {\occset}} clause is an
+be substituted in the context. The {\tt in {\occgoalset}} clause is an
 occurrence clause whose syntax and behavior is described in
 Section~\ref{Occurrences clauses}.
 
@@ -465,8 +465,8 @@ Section~\ref{Occurrences clauses}.
   is generated by {\Coq}. This variant also supports an occurrence clause.
 
 \item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term}
-      {\tt ) in {\occset}}\\
-      {\tt set {\term} in {\occset}}
+      {\tt ) in {\occgoalset}}\\
+      {\tt set {\term} in {\occgoalset}}
 
   These are the general forms which combine the previous possibilities.
 
@@ -475,7 +475,7 @@ Section~\ref{Occurrences clauses}.
   This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a
   logical (Leibniz's) equality instead of a local definition.
 
-\item {\tt remember {\term} {\tt as} {\ident} in {\occset}}
+\item {\tt remember {\term} {\tt as} {\ident} in {\occgoalset}}
 
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
@@ -900,18 +900,18 @@ An occurrences clause is a modifier to some tactics that obeys the
 following syntax:
 
 $\!\!\!$\begin{tabular}{lcl}
-{\occclause} & ::= & {\tt in} {\occset} \\
-{\occset} & ::= &
-    \zeroone{{\ident$_1$} \zeroone{{\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} {\dots} {\tt ,}
-    {\ident$_m$} \zeroone{{\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}}}\\
-&   &
-    \zeroone{{\tt |-} 
-      \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}}\\
+{\occclause} & ::= & {\tt in} {\occgoalset} \\
+{\occgoalset} & ::= &
+    \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+&   & {\dots} {\tt ,}\\
+&   & {\ident$_m$} \zeroone{\atoccurrences}}\\
+&   & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\
 & | &
-    {\tt *} {\tt |-}
-        \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}\\
+    {\tt *} {\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}\\
 & | &
     {\tt *}\\
+{\atoccurrences} & ::= & {\tt at} {\occlist}\\
+{\occlist} & ::= & \zeroone{\tt -} {\num$_1$} \dots\ {\num$_n$}
 \end{tabular}
 
 The role of an occurrence clause is to select a set of occurrences of
@@ -927,10 +927,13 @@ particular, occurrences of {\term} in implicit arguments (see
 Section~\ref{Implicit Arguments}) or coercions (see
 Section~\ref{Coercions}) are counted.
 
-A negative occurrence number means an occurrence which should not be
-substituted.  As an exception to the left-to-right order, the
-occurrences in the {\tt return} subexpression of a {\tt match} are
-considered {\em before} the occurrences in the matched term.
+If a minus sign is given between {\tt at} and the list of occurrences,
+it negates the condition so that the clause denotes all the occurrences except
+the ones explicitly mentioned after the minus sign.
+
+As an exception to the left-to-right order, the occurrences in the
+{\tt return} subexpression of a {\tt match} are considered {\em
+before} the occurrences in the matched term.
 
 In the second case, the {\tt *} on the left of {\tt |-} means that
 all occurrences of {\term} are selected in every hypothesis.
@@ -1290,10 +1293,16 @@ x}$)$) $t$}.  This command can be used, for instance, when the tactic
 \begin{Variants}
 \item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}}
   
-  Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} will be
+  Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} are
   considered for $\beta$-expansion. Occurrences are located from left
   to right.
 
+\item {\tt pattern {\term} at - {\num$_1$} \dots\ {\num$_n$}}
+  
+  All occurrences except the occurrences of indexes {\num$_1$} \dots\
+  {\num$_n$} of {\term} are considered for
+  $\beta$-expansion. Occurrences are located from left to right.
+
 \item {\tt pattern {\term$_1$}, \dots, {\term$_m$}}
   
   Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic
@@ -1310,6 +1319,11 @@ x}$)$) $t$}.  This command can be used, for instance, when the tactic
   \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$
   of \term$_m$ starting from \term$_m$.
 
+\item {\tt pattern} {\term$_1$} \zeroone{{\tt at \zeroone{-}} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} \dots {\tt ,}
+    {\term$_m$} \zeroone{{\tt at \zeroone{-}} {\num$_1^m$} \dots\ {\num$_{n_m}^m$}}
+  
+  This is the most general syntax that combines the different variants.
+
 \end{Variants}
 
 \subsection{Conversion tactics applied to hypotheses}
@@ -1524,10 +1538,10 @@ induction n.
   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 {\occset}}
+\item \texttt{induction {\term} in {\occgoalset}}
 
   This syntax is used for selecting which occurrences of {\term} the
-  induction has to be carried on. The {\tt in {\occset}} clause is an
+  induction has to be carried on. The {\tt in {\atoccurrences}} clause is an
   occurrence clause whose syntax and behavior is described in
   Section~\ref{Occurrences clause}.
 
@@ -1535,8 +1549,8 @@ induction n.
   the value it gets in each case of the induction is added to the
   context of the subgoals corresponding to the induction cases.
 
-\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\
-     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}
+\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}}
 
   This is the most general form of {\tt induction} and {\tt
   einduction}.  It combines the effects of the {\tt with}, {\tt as},
@@ -1700,10 +1714,10 @@ last introduced hypothesis.
   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 {\occset}}
+\item \texttt{destruct {\term} in {\occgoalset}}
 
   This syntax is used for selecting which occurrences of {\term} the
-  case analysis has to be done on. The {\tt in {\occset}} clause is an
+  case analysis has to be done on. The {\tt in {\occgoalset}} clause is an
   occurrence clause whose syntax and behavior is described in
   Section~\ref{Occurrences clauses}.
 
@@ -1711,8 +1725,8 @@ last introduced hypothesis.
   the value it gets in each cases of the analysis is added to the
   context of the subgoals corresponding to the cases.
 
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\
-     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}
+\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}}
 
   This is the most general form of {\tt destruct} and {\tt edestruct}.
   It combines the effects of the {\tt with}, {\tt as}, {\tt using},
@@ -2146,8 +2160,8 @@ This happens if \term$_1$ does not occur in the goal.
   \begin{itemize}
   \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
     \texttt{H1} instead of the current goal.
-  \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
-      rewrite H in H2}. In particular a failure will happen if any of
+  \item \texttt{rewrite H in H1 at 1, H2 at - 2 |- *} means \texttt{rewrite H; rewrite H in H1 at 1;
+      rewrite H in H2 at - 2}. In particular a failure will happen if any of
     these three simpler tactics fails. 
   \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
       H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
@@ -2159,7 +2173,7 @@ This happens if \term$_1$ does not occur in the goal.
   Orientation {\tt ->} or {\tt <-} can be
   inserted before the term to rewrite.
 
-\item {\tt rewrite {\term} at \textit{occurrences}}
+\item {\tt rewrite {\term} at {\occlist}}
   \tacindex{rewrite \dots\ at}
 
   Rewrite only the given occurrences of \term$_1'$. Occurrences are