diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-29 13:01:31 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-29 13:01:31 +0000 |
commit | 18373e78c9a0f171f193605ccb2556bb064b6e62 (patch) | |
tree | 35a1541e16d30c0633757fc025842bcf64451711 /doc/refman/RefMan-ltac.tex | |
parent | ca104bd655bfcf0f3d2689215c33fdedc01e5f9c (diff) |
Documenting the "appcontext" by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index f10b9c3ee..4029e4e28 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -615,20 +615,20 @@ f (3+4). \end{coq_example} \item \index{appcontext!in pattern} -For historical reasons, {\tt context} considers $n$-ary applications + \comindex{Set Tactic Compat Context} + \comindex{Unset Tactic Compat Context} +For historical reasons, {\tt context} used to consider $n$-ary applications such as {\tt (f 1 2)} as a whole, and not as a sequence of unary -applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} will fail -to find a matching subterm in {\tt (f 1 2)}: if the pattern is a partial -application, the matched subterms will be necessarily be +applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail +to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial +application, the matched subterms would have necessarily been applications with exactly the same number of arguments. -Alternatively, one may now use the following variant of {\tt context}: +As a workaround, one could use the following variant of {\tt context}: \begin{quote} {\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} \end{quote} -The behavior of {\tt appcontext} is the same as the one of {\tt - context}, except that a matching subterm could be a partial -part of a longer application. For instance, in {\tt (f 1 2)}, -an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. +This syntax is now deprecated, as {\tt context} behaves as intended. The former +behaviour can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} |