Enforcing a stronger difference between the two syntaxes "simpl

reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.

In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
  head symbol is written "+" (in the toplevel scope); idem for
  vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
  implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
  native_compute with functor application should now work (i.e.
  vm_compute and native_compute are now taken into account in
  tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
  eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.

By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").

1 files changed, 19 insertions, 13 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 75ba90f032..5c87b12cc0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3080,16 +3080,17 @@ The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
 
 These tactics apply to any goal. They try to reduce a term to
 something still readable instead of fully normalizing it. They perform
-a sort of strong normalisation with two key differences:
+a sort of strong normalization with two key differences:
 \begin{itemize}
-\item They unfold a constant if and only if it leads to an
-  $\iota$-reduction, i.e. reducing a match or unfold a fixpoint.
-\item While reducing (co)fixpoints, the tactics use the name of the
+\item They unfold a constant if and only if it leads to a
+  $\iota$-reduction, i.e. reducing a match or unfolding a fixpoint.
+\item While reducing a constant unfolding to (co)fixpoints, 
+  the tactics use the name of the
   constant the (co)fixpoint comes from instead of the (co)fixpoint
   definition in recursive calls.
 \end{itemize}
 
-The \texttt{cbn} tactic claims to be a more principled, faster and more
+The \texttt{cbn} tactic is claimed to be a more principled, faster and more
 predictable replacement for \texttt{simpl}.
 
 The \texttt{cbn} tactic accepts the same flags as \texttt{cbv} and
@@ -3169,27 +3170,32 @@ reduced to \texttt{S t}.
   [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbn beta delta
   -[\qualid$_1$\ldots\qualid$_k$] iota zeta} (see \ref{vmcompute}).
 
-\item {\tt simpl {\term}}
+\item {\tt simpl {\pattern}}
 
-  This applies {\tt simpl} only to the occurrences of {\term} in the
+  This applies {\tt simpl} only to the subterms matching {\pattern} in the
   current goal.
 
-\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\pattern} at \num$_1$ \dots\ \num$_i$}
 
   This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
-  occurrences of {\term} in the current goal.
+  occurrences of the subterms matching {\pattern} in the current goal.
 
   \ErrMsg {\tt Too few occurrences}
 
-\item {\tt simpl {\ident}}
+\item {\tt simpl {\qualid}}\\
+  {\tt simpl {\qstring}}
 
   This applies {\tt simpl} only to the applicative subterms whose head
-  occurrence is {\ident}.
+  occurrence is the unfoldable constant {\qualid} (the constant can be
+  referred to by its notation using {\qstring} if such a notation
+  exists).
 
-\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\qualid} at \num$_1$ \dots\ \num$_i$}\\
+  {\tt simpl {\qstring} at \num$_1$ \dots\ \num$_i$}\\
 
   This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
-applicative subterms whose head occurrence is {\ident}.
+  applicative subterms whose head occurrence is {\qualid} (or
+  {\qstring}).
 
 \end{Variants}