Remove deprecated option Tactic Compat Context.

And some code simplification.

13 files changed, 39 insertions, 95 deletions

diff --git a/API/API.mli b/API/API.mli
index 3ed008ff5..3f52ac62b 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3853,10 +3853,9 @@ sig
   type matching_result =
     { m_sub : bound_ident_map * Ltac_pretype.patvar_map;
       m_ctx : EConstr.constr }
-  val match_subterm_gen : Environ.env -> Evd.evar_map ->
-                          bool ->
-                          binding_bound_vars * Pattern.constr_pattern -> EConstr.constr ->
-                          matching_result IStream.t
+  val match_subterm : Environ.env -> Evd.evar_map ->
+                      binding_bound_vars * Pattern.constr_pattern -> EConstr.constr ->
+                      matching_result IStream.t
   val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map
 end
 
diff --git a/lib/flags.ml b/lib/flags.ml
index ddc8f8482..5079b4b01 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -200,7 +200,6 @@ let native_compiler = ref false
 (* 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
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
 
diff --git a/lib/flags.mli b/lib/flags.mli
index c4afb8318..8825390e6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -160,10 +160,6 @@ val 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. *)
-
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 8b9eb3983..872bea612 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -242,12 +242,11 @@ GEXTEND Gram
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        let mode = not (!Flags.tactic_context_compat) in
-        Subterm (mode, oid, pc)
+        Subterm (oid, pc)
       | IDENT "appcontext";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
         warn_deprecated_appcontext ~loc:!@loc ();
-        Subterm (true,oid, pc)
+        Subterm (oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
   match_hyps:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6aa2f6f89..e5ff47356 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s =
 
   let pr_match_pattern pr_pat = function
     | Term a -> pr_pat a
-    | Subterm (b,None,a) ->
-    (** ppedrot: we don't make difference between [appcontext] and [context]
-        anymore, and the interpretation is governed by a flag instead. *)
+    | Subterm (None,a) ->
       keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
-    | Subterm (b,Some id,a) ->
+    | Subterm (Some id,a) ->
       keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
 
   let pr_match_hyps pr_pat = function
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9bd3efc6b..ccd555b61 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
-  | Subterm of bool * Id.t option * 'a
+  | Subterm of Id.t option * 'a
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index b16b0a7ba..ebffde441 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) =
 
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) ltacvars = function
-  | Subterm (b,ido,pc) ->
+  | Subterm (ido,pc) ->
       let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
-      ido, metas, Subterm (b,ido,pc)
+      ido, metas, Subterm (ido,pc)
   | Term pc ->
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       None, metas, Term pc
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e0d7eca5f..d190cc2cd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) =
     (bvars,instantiate_pattern env sigma lfun pat)
 
 let read_pattern lfun ist env sigma = function
-  | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+  | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c)
   | Term c -> Term (eval_pattern lfun ist env sigma c)
 
 (* Reads the hypotheses of a Match Context rule *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 918d1faeb..79bf3685e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc))
+  | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc))
   | Term pc -> Term (subst_glob_constr_or_pattern subst pc)
 
 let rec subst_match_goal_hyps subst = function
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 89b78e590..e87951dd7 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             return lhs
           with Constr_matching.PatternMatchingFailure -> fail
         end
-    | Subterm (with_app_context,id_ctxt,p) ->
+    | Subterm (id_ctxt,p) ->
 
       let rec map s (e, info) =
         { stream = fun k ctx -> match IStream.peek s with
@@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
+      map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 478ba73fd..ec7c3077f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -206,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
   in
   constrain sigma n c subst
       
-let matches_core env sigma allow_partial_app allow_bound_rels
+let matches_core env sigma allow_bound_rels
     (binding_vars,pat) c =
   let open EConstr in
   let convref ref c = 
@@ -260,7 +260,7 @@ let matches_core env sigma allow_partial_app allow_bound_rels
       | PApp (PApp (h, a1), a2), _ ->
           sorec ctx env subst (PApp(h,Array.append a1 a2)) t
 
-      | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
+      | PApp (PMeta meta,args1), App (c2,args2) ->
          (let diff = Array.length args2 - Array.length args1 in
           if diff >= 0 then
             let args21, args22 = Array.chop diff args2 in
@@ -373,14 +373,14 @@ let matches_core env sigma allow_partial_app allow_bound_rels
   in
   sorec [] env (Id.Map.empty, Id.Map.empty) pat c
 
-let matches_core_closed env sigma allow_partial_app pat c =
-  let names, subst = matches_core env sigma allow_partial_app false pat c in
+let matches_core_closed env sigma pat c =
+  let names, subst = matches_core env sigma false pat c in
   (names, Id.Map.map snd subst)
 
-let extended_matches env sigma = matches_core env sigma true true
+let extended_matches env sigma = matches_core env sigma true
 
 let matches env sigma pat c =
-  snd (matches_core_closed env sigma true (Id.Set.empty,pat) c)
+  snd (matches_core_closed env sigma (Id.Set.empty,pat) c)
 
 let special_meta = (-1)
 
@@ -405,9 +405,9 @@ let matches_head env sigma pat c =
   matches env sigma pat head
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ env sigma partial_app closed pat c mk_ctx =
+let authorized_occ env sigma closed pat c mk_ctx =
   try
-    let subst = matches_core_closed env sigma partial_app pat c in
+    let subst = matches_core_closed env sigma pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
     then (fun next -> next ())
     else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
@@ -416,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx =
 let subargs env v = Array.map_to_list (fun c -> (env, c)) v
 
 (* Tries to match a subterm of [c] with [pat] *)
-let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
+let sub_match ?(closed=true) env sigma pat c =
   let open EConstr in
   let rec aux env c mk_ctx next =
-  let here = authorized_occ env sigma partial_app closed pat c mk_ctx in
+  let here = authorized_occ env sigma closed pat c mk_ctx in
   let next () = match EConstr.kind sigma c with
   | Cast (c1,k,c2) ->
       let next_mk_ctx = function
@@ -449,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
-        let topdown = true in
-        if partial_app then
-          if topdown then
-            let lc1 = Array.sub lc 0 (Array.length lc - 1) in
-            let app = mkApp (c1,lc1) in
-            let mk_ctx = function
-              | [app';c] -> mk_ctx (mkApp (app',[|c|]))
-              | _ -> assert false in
-            try_aux [(env, app); (env, Array.last lc)] mk_ctx next
-          else
-            let rec aux2 app args next =
-              match args with
-              | [] ->
-                  let mk_ctx le =
-                    mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-                  let sub = (env, c1) :: subargs env lc in
-                  try_aux sub mk_ctx next
-              | arg :: args ->
-                  let app = mkApp (app,[|arg|]) in
-                  let next () = aux2 app args next in
-                  let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
-                  aux env app mk_ctx next in
-            aux2 c1 (Array.to_list lc) next
-        else
-          let mk_ctx le =
-            mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-          let sub = (env, c1) :: subargs env lc in
-          try_aux sub mk_ctx next
+     let lc1 = Array.sub lc 0 (Array.length lc - 1) in
+     let app = mkApp (c1,lc1) in
+     let mk_ctx = function
+       | [app';c] -> mk_ctx (mkApp (app',[|c|]))
+       | _ -> assert false in
+     try_aux [(env, app); (env, Array.last lc)] mk_ctx next
   | Case (ci,hd,c1,lc) ->
       let next_mk_ctx = function
       | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
@@ -499,14 +477,11 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
     let sub = subargs env types @ subargs env bodies in
     try_aux sub next_mk_ctx next
   | Proj (p,c') ->
-    let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
-      if partial_app then
-	try 
-	  let term = Retyping.expand_projection env sigma p c' [] in
-	    aux env term mk_ctx next
-	with Retyping.RetypeError _ -> next ()
-      else
-      try_aux [env, c'] next_mk_ctx next
+    begin try
+      let term = Retyping.expand_projection env sigma p c' [] in
+      aux env term mk_ctx next
+    with Retyping.RetypeError _ -> next ()
+    end
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
     next ()
   in
@@ -527,13 +502,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
 
-let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c
-
-let match_appsubterm env sigma pat c = 
-  sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c
-
-let match_subterm_gen env sigma app pat c = 
-  sub_match ~partial_app:app env sigma pat c
+let match_subterm env sigma pat c = sub_match env sigma pat c
 
 let is_matching env sigma pat c =
   try let _ = matches env sigma pat c in true
@@ -545,5 +514,5 @@ let is_matching_head env sigma pat c =
 
 let is_matching_appsubterm ?(closed=true) env sigma pat c =
   let pat = (Id.Set.empty,pat) in
-  let results = sub_match ~partial_app:true ~closed env sigma pat c in
+  let results = sub_match ~closed env sigma pat c in
   not (IStream.is_empty results)
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 60e1c34a1..e4d9ff9e1 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -61,18 +61,10 @@ type matching_result =
     { m_sub : bound_ident_map * patvar_map;
       m_ctx : EConstr.t }
 
-(** [match_subterm n pat c] returns the substitution and the context
-   corresponding to each **closed** subterm of [c] matching [pat]. *)
-val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
-
-(** [match_appsubterm pat c] returns the substitution and the context
+(** [match_subterm pat c] returns the substitution and the context
    corresponding to each **closed** subterm of [c] matching [pat],
    considering application contexts as well. *)
-val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
-
-(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : env -> Evd.evar_map ->
-  bool (** true = with app context *) ->
+val match_subterm : env -> Evd.evar_map ->
   binding_bound_vars * constr_pattern -> constr ->
   matching_result IStream.t
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cc5593f3f..bf05c9b83 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,14 +59,6 @@ let typ_of env sigma c =
 
 open Goptions
 
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      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 apply_solve_class_goals = ref false
 
 let _ =