From 18373e78c9a0f171f193605ccb2556bb064b6e62 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 29 May 2013 13:01:31 +0000 Subject: Documenting the "appcontext" by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-ltac.tex | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'doc/refman') 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} -- cgit v1.2.3