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
---
 CHANGES                    |  3 +++
 doc/refman/RefMan-ltac.tex | 18 +++++++++---------
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/CHANGES b/CHANGES
index d79b1d02ff..00c59fa166 100644
--- a/CHANGES
+++ b/CHANGES
@@ -46,6 +46,9 @@ Tactics
 - "change ... in ..." and "simpl ... in ..." now consider nested
   occurrences (possible source of incompatibilities since this alters
   the numbering of occurrences).
+- Now "appcontext" and "context" behave the same. The old buggy behaviour of
+  "context" can be retrieved at parse time by setting the
+  "Tactic Compat Context" flag. (possible source of incompatibilities).
 
 
 Program
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index f10b9c3ee5..4029e4e28e 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