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

1 files changed, 12 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ab962a4cc..0595a7789 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;