From 02dddc0fd65eff35fe00a180e99a2816ab2c6b6a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 28 May 2013 22:51:36 +0000
Subject: Setting "appcontext" as the default behaviour in Ltac matching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_ltac.ml4 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 79f532781d..482f0df721 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Compat
 open Constrexpr
 open Tacexpr
@@ -163,9 +164,11 @@ GEXTEND Gram
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        Subterm (false,oid, pc)
+        let mode = not (!Flags.tactic_context_compat) in
+        Subterm (mode, oid, pc)
       | IDENT "appcontext";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
+        msg_warning (strbrk "appcontext is deprecated");
         Subterm (true,oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
-- 
cgit v1.2.3