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

4 files changed, 22 insertions, 1 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d8355e3e10..f62ed20e5d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -175,3 +175,5 @@ let no_native_compiler = ref Coq_config.no_native_compiler
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 let print_mod_uid = ref false
+
+let tactic_context_compat = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 3965713fe2..c170c2669a 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -104,3 +104,7 @@ val no_native_compiler : bool ref
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 val print_mod_uid : bool ref
+
+val tactic_context_compat : bool ref
+(** Set to [true] to trigger the compatibility bugged context matching (old
+    context vs. appcontext) is set. *)
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 ] ]
   ;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ab962a4cc3..0595a7789a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -65,11 +65,14 @@ let typ_of = Retyping.get_type_of
 (* Option for 8.2 compatibility *)
 open Goptions
 let dependent_propositions_elimination = ref true
+let tactic_compat_context = ref false
 
 let use_dependent_propositions_elimination () =
   !dependent_propositions_elimination
   && Flags.version_strictly_greater Flags.V8_2
 
+let use_tactic_context_compat () = !tactic_compat_context
+
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -79,6 +82,15 @@ let _ =
       optread  = (fun () -> !dependent_propositions_elimination) ;
       optwrite = (fun b -> dependent_propositions_elimination := b) }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "trigger bugged context matching compatibility";
+      optkey   = ["Tactic";"Compat";"Context"];
+      optread  = (fun () -> !Flags.tactic_context_compat) ;
+      optwrite = (fun b -> Flags.tactic_context_compat := b) }
+
 let tactic_infer_flags = {
   Pretyping.use_typeclasses = true;
   Pretyping.use_unif_heuristics = true;